Matematikawan mulai mengerjakan pembuktian komputer untuk teka-teki 350 tahun, 'Teorema Terakhir Fermat'
(dongascience.com)Teorema Terakhir Fermat akan dibuktikan ulang dalam bahasa komputer
- Profesor Kevin Buzzard dari Imperial College London berencana menulis pembuktian formal Teorema Terakhir Fermat (FLT) menggunakan pembukti teorema Lean mulai Oktober 2024.
- Engineering and Physical Sciences Research Council [EPSRC] di Inggris telah memutuskan untuk mendanai Profesor Buzzard selama lima tahun mulai bulan tersebut.
- Dokumen rencana proyek yang dibuat dengan Lean blueprints, sebuah plugin plasTeX, dijadwalkan akan dipublikasikan pada akhir April 2024.
Bukankah Teorema Terakhir Fermat sudah dibuktikan?
Sudah. Matematikawan Inggris Andrew Wiles mempublikasikan pembuktiannya pada 1994, dan pembuktian itu diterbitkan secara resmi pada 1995. Namun, pembuktian formal yang ditulis dalam bahasa interactive theorem prover [ITP] masih belum ada.
Interactive theorem prover? Pembuktian formal? Apa itu?
- interactive theorem prover [ITP]: program komputer yang membantu manusia menulis pembuktian formal. Juga disebut proof assistant.
- pembuktian formal: pembuktian yang dapat diverifikasi oleh program komputer bernama proof verifier. Proof assistant biasanya juga berperan sebagai proof verifier.
Apakah theorem prover itu kecerdasan buatan?
Neural theorem prover [NTP] bisa dianggap demikian, tetapi banyak interactive theorem prover termasuk Lean bukanlah program berbasis machine learning.
Tolong perkenalkan pembukti teorema Lean.
- Interactive theorem prover sekaligus bahasa pemrograman fungsional murni.
- Berbasis dependent type theory.
- Memiliki fitur seperti type class, sintaks yang dapat diperluas, macro, dan metaprogramming.
- Dibanding proof assistant lain, basis pengguna Lean mencakup terutama banyak matematikawan yang meneliti bidang di luar fondasi matematika.
Mengapa ingin menulis pembuktian formal untuk Teorema Terakhir Fermat?
Mengutip postingan Profesor Kevin Buzzard di X, "tujuannya adalah membuat komputer memahami teori bilangan modern, sehingga pada akhirnya dapat membantu para ahli teori bilangan."
Tautan
- Pesan yang diunggah Profesor Kevin Buzzard di chat Zulip Lean pada 3 Oktober 2023: https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/…
- Pustaka matematika Lean: https://github.com/leanprover-community/mathlib4
- Artikel New Scientist: https://institutions.newscientist.com/article/…
- Artikel Popular Mechanics: https://popularmechanics.com/science/math/…
1 komentar
Saya mendukungnya. Bagi yang tertarik dengan formal proof, saya juga merekomendasikan untuk menonton kuliah Prof. Terrence Tao, Machine Assisted Proofs (https://www.youtube.com/watch?v=AayZuuDDKP0).