Claude susun bukti formal Teorema Terakhir Fermat di Lean

Peneliti Anthropic memakai Claude untuk menghasilkan bukti Teorema Terakhir Fermat pertama yang diverifikasi komputer di Lean, proof assistant yang dipakai matematikawan untuk memeriksa argumen baris demi baris. Proyek yang dipimpin Tianyi Peng ini rampung dalam 11 hari dan menghasilkan sekitar 13 juta baris kode Lean, dengan 30.300 teorema terbukti dan 29.500 di antaranya masuk ke hasil akhir. Claude mengikuti versi ringkas bukti Andrew Wiles tahun 1995, dan prosesnya menghabiskan kira-kira 6 miliar output token dari sebuah model riset internal.

Bagian yang menarik adalah cara kerjanya dikoordinasikan. Claude bekerja hampir sepenuhnya mandiri lewat platform bernama Prove2Me, yang menyimpan graf pernyataan teorema sehingga banyak agent bisa membagi tugas, melakukan kompilasi paralel, dan memakai ulang hasil sebelumnya dengan mencari deskripsi bahasa biasa dari tiap lemma. Bukti yang jadi berukuran lebih dari lima kali Mathlib, library matematika formal utama milik komunitas.

Kevin Buzzard dari Imperial College London, yang memimpin upaya terpisah dan berjangka panjang untuk memformalkan teorema yang sama secara manual, menilai capaian ini menunjukkan formalisasi otomatis atas literatur matematika modern kini mulai terjangkau. Menurutnya, itu bisa menangkap kesalahan pada bukti yang sudah terbit sekaligus meringankan beban penelaah. Metodenya bisa dibaca lengkap di tulisan Anthropic.

Kenapa ini penting

Bagi Anda yang bekerja di matematika atau verifikasi formal, titik hambatnya bergeser: bukti terverifikasi mesin untuk hasil yang rumit tidak lagi menuntut kerja manusia bertahun-tahun. Yang jadi pertanyaan sekarang adalah seberapa jauh Anda memercayai perkakasnya dan mampu mengaudit apa yang benar-benar dihasilkan model.