Para peneliti berkumpul di London minggu ini untuk mempercepat formalisasi Teorema Terakhir Fermat menggunakan model AI canggih. Lokakarya ini berfokus pada pengubahan bukti Andrew Wiles tahun 1993 menjadi kode Lean untuk verifikasi komputer. Kemajuan berlangsung pesat, dengan jumlah baris kode meningkat dua kali lipat setelah hari pertama.
Dua puluh lima matematikawan, ilmuwan komputer, dan pakar AI bertemu di sebuah hotel di pusat kota London untuk mengerjakan proyek yang dipimpin oleh Kevin Buzzard dari Imperial College London. Upaya lima tahun yang didanai pada tahun 2024 ini bertujuan untuk menambahkan teorema tersebut ke dalam repositori matematika formal, Mathlib.
Sebelum lokakarya dimulai, terdapat 20.000 baris kode dalam proyek tersebut. Setelah hari pertama, jumlahnya mencapai 40.000. Buzzard mencatat bahwa kemampuan AI meningkat tajam sejak Desember tahun lalu, yang memungkinkan tim untuk menangani lebih banyak aspek matematika dasar daripada yang direncanakan sebelumnya.
Hang Lu Su, yang juga berasal dari Imperial College London, menggambarkan proses ini sebagai industrialisasi kerja intelektual. Para peserta menggunakan model termasuk Claude untuk membuat dan menyempurnakan kode, meskipun masih ada kekhawatiran mengenai verbositas dan pemeliharaan jangka panjang dari output yang dihasilkan AI.
Buzzard menyatakan keyakinannya bahwa tujuan awal akan tercapai pada akhir proyek. Sejauh mana tim akan maju dalam menyelesaikan seluruh piramida teorema pendukung akan bergantung pada perkembangan AI lebih lanjut.