Claude memformalkan Teorema Terakhir Fermat dalam Lean
Anthropic melaporkan pada 4 September 2026 bahwa Claude menghasilkan bukti lengkap pertama Teorema Terakhir Fermat yang diverifikasi komputer, menulis sekitar 13 juta baris Lean dan membuktikan sekitar 29.500 teorema perantara dalam sekitar 11 hari kerja multi-agen yang sebagian besar otonom di platform Prove2Me, dengan memakai tiga aksioma standar Lean dan pernyataan yang cocok dengan FLT di Mathlib. Peneliti Anthropic Tianyi Peng mengarahkan prioritas tingkat tinggi; Kevin Buzzard meninjau hasilnya dan menyebut autoformalisasi tersebut luar biasa, serta mengatakan teknik semacam ini dapat membantu memeriksa matematika buatan AI dan meringankan proses telaah sejawat. Anthropic membingkai ini sebagai verifikasi jalur teorema Wiles (lewat Darmon–Diamond–Taylor), bukan matematika baru seperti hasil Riemann yang baru, dan bukan peluncuran produk konsumen Claude.
Diterjemahkan dengan bantuan AI.