AI mengubah teorema terakhir Fermat menjadi pembuktian Lean terbesar sejauh ini

Teorema terakhir Fermat untuk pertama kalinya diterjemahkan menjadi kode yang dapat diperiksa komputer, menghasilkan pembuktian formal sepanjang 13 juta baris hanya dalam 11 hari. Sekelompok agen AI mengembangkan sekitar 29.500 teorema perantara yang diperlukan untuk menyelesaikan pekerjaan tersebut dalam Lean, bahasa pemrograman yang dirancang untuk memverifikasi logika matematika.

Pencapaian ini tidak menggantikan atau memperluas pembuktian yang diselesaikan oleh Andrew Wiles dan Richard Taylor pada 1990-an. Sebaliknya, pencapaian ini mengubah penalaran yang sudah mapan tersebut menjadi bentuk yang dapat diperiksa komputer langkah demi langkah. Teorema itu menyatakan bahwa tidak ada bilangan bulat yang dapat memenuhi aⁿ + bⁿ = cⁿ ketika n lebih besar dari 2.

Para ahli manusia sesekali memberikan arahan umum. Agen-agen tersebut pada awalnya kesulitan berkoordinasi, tetapi berhasil setelah menggunakan Prove2Me, alat kolaborasi yang membantu mereka melacak tugas yang telah selesai dan memilih pekerjaan berikutnya. Matematikawan Kevin Buzzard mengompilasi kode yang dihasilkan dan menjalankan pemeriksaan standar Lean, lalu menyimpulkan bahwa kode itu benar-benar mengembangkan kerangka matematika yang diperlukan.

Formalisasi ini berukuran lebih dari lima kali ukuran Mathlib, pustaka bersama utama untuk matematika dalam Lean. Skalanya menunjukkan bahwa AI mungkin segera membantu mengubah bagian-bagian besar dari literatur matematika menjadi kode yang dapat diverifikasi, meskipun meninjau keluaran sebesar itu dan membuatnya dapat dipahami manusia tetap menjadi tantangan besar.