Perusahaan AI matematika Axiom mengumumkan bahwa kawanan agen AxiomProver miliknya menyelesaikan formalisasi Lean atas Teorema Klasifikasi Grup Sederhana Hingga (CFSG) dalam 24 hari, dan menyebutnya sebagai bukti lengkap pertama yang diperiksa komputer untuk teorema ini. Kodenya dibuka di GitHub dengan lisensi Apache-2.0. Repositori menyatakan versi akhirnya tidak memuat placeholder sorry, tidak memakai native_decide, dan hanya bergantung pada tiga aksioma standar: ekstensionalitas proposisi, aksioma pilihan klasik, dan kesehihan (soundness) hasil bagi.
Klasifikasi grup sederhana hingga sering disebut "tabel periodik simetri." Teorema ini menyatakan bahwa setiap grup sederhana hingga termasuk salah satu dari 18 keluarga tak hingga, atau salah satu dari 26 grup sporadis. Bukti aslinya tersebar di lebih dari 500 makalah dengan total sekitar 15.000 halaman, ditulis oleh sekitar 100 matematikawan sejak sekitar 1955 hingga 2004. Bagian terakhir, kasus quasithin oleh Aschbacher dan Smith, saja sudah setebal 1.221 halaman.
Apa yang terjadi dalam 24 hari itu
Menurut proses yang dipublikasikan Axiom, proyek ini membuat grup kolaborasi Slack pada 1 Oktober, dan gelombang pertama agen mulai aktif pada 2 Oktober. Seluruh bukti dipecah menjadi 108 tonggak dan sekitar 380 tugas kecil. Para agen mengambil tugas lewat issue GitHub dan melaporkan kemajuan di Slack. Agen utama bertugas memecah masalah dan meninjau pernyataan, sedangkan agen lainnya mencari hasil yang sudah ada atau menulis bukti Lean, lalu meneruskan pekerjaan ke bawah ketika ada prasyarat yang belum tersedia.
Jalannya tidak mulus. Satu gelombang kode awal dihapus seluruhnya karena asumsi tersirat yang keliru, dan tim harus merencanakan ulang. Setelah itu kecepatan build menjadi hambatan; para insinyur memakai cache dan pemeriksaan paralel, serta memindahkan komputasi hingga ke luar dalam bentuk sertifikat yang dapat diverifikasi, sehingga build penuh bisa ditekan di bawah 24 jam. Pada 10 Oktober, proyek ini secara terpisah mengumumkan bukti bahwa grup Monster adalah grup sederhana.
Soal korpus, Axiom menyebut total 715 makalah dan buku dibaca, dan proyek ini memakai ulang sekitar 1,2 juta baris kode dari proyek Qiuzhen-CFSG sebelumnya, serta pustaka formal yang sudah ada seperti Mathlib dan Tau Ceti.
Kesalahan yang ikut terjaring
Selama formalisasi, tim mencatat 34 penyimpangan matematis yang cukup jelas. Yang paling disorot ada pada jalur "Teorema Grup Tak Seimbang" (UGT): sebuah klaim penutupan dalam memoar Walter tahun 1986 memiliki contoh tandingan, yaitu bermula dari PSL₂(49) akan sampai ke PSL₂(7), padahal grup yang terakhir ini justru dikecualikan dari keluarga tersebut. Sebuah lema Aschbacher–Smith juga ditemukan memiliki contoh tandingan SL₂(5); setelah kesamaan diubah menjadi ketidaksamaan, argumen sesudahnya harus diperluas.
Axiom menerbitkan makalah tersendiri setebal 35 halaman yang mengusulkan argumen pengganti, dan memperbaiki jalur ini dengan melibatkan para penasihat seperti Lyons dan Solomon. Perusahaan berulang kali menegaskan bahwa contoh tandingan ini tidak membatalkan UGT itu sendiri, apalagi menggoyahkan teorema klasifikasi.
"the classification remains the achievement of the mathematicians who discovered the groups"
(Klasifikasi tetap menjadi capaian para matematikawan yang menemukan grup-grup itu.)
Dibandingkan verifikasi mesin sebelumnya
Pembanding yang paling sering dipakai adalah verifikasi Teorema Orde Ganjil oleh tim Gonthier di Coq pada 2012. Teorema itu bersumber dari makalah Feit dan Thompson tahun 1963 setebal 255 halaman; proyeknya memakan waktu sekitar enam tahun dan menjadi salah satu batu penjuru bukti klasifikasi. Cakupan Axiom kali ini adalah seluruh bangunan, dengan waktu yang dihitung dalam hari.
Keduanya tidak bisa langsung dibandingkan dari sisi kecepatan. Proyek Orde Ganjil dulu membangun pustakanya hampir dari nol, sedangkan Axiom berdiri di atas Mathlib dan 1,2 juta baris kode CFSG sebelumnya, dengan jumlah agen "puluhan." Daya komputasi, perangkat keras, dan total biaya di baliknya tidak diungkap, begitu pula jumlah jam kerja manusia. Angka 24 hari adalah durasi proyek formalisasi itu sendiri, tidak termasuk puluhan tahun kerja manusia yang menjadi landasannya.
Beberapa catatan keberatan juga dituliskan secara terbuka. Metadata proyek menandai peninjauan sebagai "penilaian mandiri," dan belum ada pihak ketiga yang mereproduksi build penuh dari lingkungan bersih. Pemeriksaan mesin hanya menjamin bahwa penurunan logis sahih bertolak dari asumsi yang tertulis; apakah definisi dalam pernyataan klasifikasi setia pada teorema aslinya tetap harus diperiksa satu per satu oleh pakar teori grup. Makalah UGT itu terbit di platform pracetak tanpa tinjauan sejawat, dan daftar errata, kata Axiom, akan dipasang di halaman proyek.
Bagi para pelaku formalisasi, ada dua hal yang perlu dicermati berikutnya: apakah komunitas dapat menjalankan 43,1 juta baris ini secara mandiri, dan berapa banyak dari 34 penyimpangan itu yang dapat dikonfirmasi oleh pihak penulis aslinya.
Sumber: pengumuman proyek Axiom dan repositori GitHub, Unite.AI, CocoLoop, Kingy AI. Jumlah baris kode Lean, jumlah deklarasi, jumlah tonggak, dan jumlah penyimpangan mengikuti angka yang dipublikasikan Axiom; durasi verifikasi Teorema Orde Ganjil berdasarkan materi Microsoft Research.