Axiom Math Merilis Bukti Lean Klasifikasi Grup Sepanjang 43,1 Juta Baris

Pada 27 Oktober 2026, Axiom Math mengatakan bahwa perusahaan itu merilis apa yang disebutnya sebagai bukti pertama Klasifikasi Grup Sederhana Berhingga yang sepenuhnya diperiksa komputer. Bukti ini disusun selama 24 hari oleh para insinyur dan matematikawan yang mengarahkan puluhan agen AI dalam jumlah besar, yang menulis sekitar 43,1 juta baris kode menggunakan asisten pembuktian Lean.

“Hari ini, kami merilis bukti pertama Klasifikasi Grup Sederhana Berhingga (CFSG) yang sepenuhnya diperiksa komputer,” tulis perusahaan itu dalam pengumumannya. Klasifikasi ini mengidentifikasi unsur-unsur dasar pembentuk grup berhingga. Bukti aslinya mencakup sekitar 15.000 halaman dalam lebih dari 500 artikel karya sekitar 100 matematikawan—skala yang membuatnya dijuluki teorema raksasa.

Apa yang Dirilis Axiom

CFSG menetapkan bahwa setiap grup sederhana berhingga adalah grup siklik berorde prima, grup alternating pada sedikitnya lima simbol, salah satu dari enam belas keluarga tak berhingga grup tipe Lie yang dibangun di atas medan berhingga, atau salah satu dari tepat 26 grup sporadis yang terisolasi. Pengumuman itu mencatat bahwa beberapa penulis menghitung grup Tits sebagai grup ke-27. Grup sporadis terbesar, Monster, dibangun oleh Robert Griess pada 1980 menggunakan aljabar berdimensi 196.884.

Upaya manusia membuktikan teorema ini berlangsung selama beberapa dekade. Pada 1963, Walter Feit dan John Thompson membuktikan bahwa setiap grup sederhana berhingga nonabelian berorde genap, dalam sebuah makalah setebal 255 halaman yang mengisi satu edisi penuh Pacific Journal of Mathematics. Pada 1972, Daniel Gorenstein memaparkan program enam belas langkah untuk menuntaskan klasifikasi tersebut dan menyatakan bahwa program itu telah selesai pada 1983. Namun, kasus kuasitebal masih bergantung pada manuskrip Geoffrey Mason yang belum rampung hingga Michael Aschbacher dan Stephen Smith menerbitkan pembahasan sepanjang 1.221 halaman pada 2004, menuntaskan apa yang kemudian dikenal sebagai bukti generasi pertama. Bukti generasi kedua yang lebih sistematis, yang dimulai oleh Gorenstein dan Richard Lyons, lalu dilanjutkan bersama Ronald Solomon dan Inna Capdeboscq, masih belum rampung. Karena itu, Axiom memformalkan bukti generasi pertama.

Halaman proyek menyebut formalisasi ini mengikuti bukti generasi pertama, dengan setiap langkah logis diperiksa oleh kernel Lean. Halaman itu mencantumkan 43,1 juta baris kode Lean, 2,05 juta deklarasi, serta 715 makalah dan buku dalam korpusnya. Axiom mengatakan peta buktinya merujuk pada jilid-jilid bukti generasi kedua dan formalisasi tersebut menggabungkan sekitar 1,2 juta baris kode dari proyek Qiuzhen-CFSG sebelumnya. Proyek ini juga dibangun di atas Mathlib, yang menurut Axiom merupakan hasil kerja ratusan kontributor. Proyek tersebut mencantumkan Dean Cureton, Vasily Ilin, Bhavik Mehta, dan Niels Voss sebagai kontributor inti, dengan Letong Hong sebagai peneliti utama.

Repositori GitHub publik menjelaskan hasil tersebut sebagai bukti Lean4 tanpa penggunaan `sorry`, yang dikunci pada versi 4.35.0-rc3, dibangun di atas Mathlib dan proyek TauCeti, serta hanya menggunakan aksioma standar Classical.choice, propext, dan Quot.sound, tanpa native_decide. Pernyataan formal klasifikasi dalam repositori itu, yang diambil dari TauCeti, berbunyi: “Setiap grup sederhana berhingga isomorfik dengan salah satu grup yang dibangun secara eksplisit dalam daftar klasifikasi.” README menyebutkan bahwa lake build memeriksa seluruh pengembangan tersebut. Perubahan terbuka pada alat pembangunan Lake dan optimisasi yang direncanakan tim untuk diajukan ke proyek induk telah memangkas waktu pembangunan hingga kurang dari 24 jam. Kode tersebut menggunakan lisensi Apache-2.0.

Upaya Kolaboratif 24 Hari dengan Puluhan Agen

Pada 1 Oktober 2026, Axiom membuka kanal Slack untuk mengoordinasikan proyek tersebut. Pekerjaan Lean yang sudah ada dan peta bukti internal yang disusun dari literatur terbitan membagi upaya ini menjadi 108 tonggak dan sekitar 380 tugas yang lebih kecil. Kawanan agen pertama mulai bekerja pada 2 Oktober 2026; para agen mengambil tonggak melalui isu GitHub dan melaporkan pekerjaan yang telah selesai di Slack. Agen utama menguraikan argumen sulit dan meninjau pernyataan, sedangkan agen lain mencari hasil yang sudah ada atau menulis bukti Lean. Para agen juga dapat mendelegasikan prasyarat yang belum terpenuhi kepada agen lain, yang hasilnya kemudian dimasukkan ke repositori bersama.

Kemajuan awal mengungkap sejumlah kelemahan. Beberapa tonggak yang tampak mudah ternyata menyembunyikan prasyarat besar yang diasumsikan oleh para agen, bukan dibuktikan. Tim pun menghapus puluhan ribu baris kode yang bertumpu pada asumsi tersebut sebelum memulai kembali dengan rencana yang lebih kokoh. Salah satu tonggak awal membahas teorema funktor signalizer; bukti kandidatnya bergantung pada asumsi struktural yang masih perlu dibuktikan. Waktu pembangunan juga menjadi hambatan ketika para agen menghasilkan bukti lebih cepat daripada kemampuan Lean untuk memeriksanya kembali. Axiom mengatakan para insinyurnya membagikan hasil pembangunan tersimpan ke sejumlah pekerja, menjalankan pemeriksaan independen secara paralel, dan memisahkan perhitungan berhingga yang mahal ke dalam sertifikat yang dapat diperiksa secara terpisah. Menurut perusahaan itu, perubahan tersebut mempercepat verifikasi hingga beberapa orde magnitudo.

Pada 10 Oktober 2026, sebuah pesan di kanal tersebut mengumumkan bahwa para agen telah membuktikan Monster sebagai grup sederhana, demikian menurut perusahaan itu. Para agen juga memformalkan keberadaan Monster melalui aljabar Griess serta sebuah teorema yang mengidentifikasi grup bertipe Monster dengan Monster. Pada 13 Oktober 2026, hanya satu tonggak yang berhasil dituntaskan. Para insinyur lalu menyusun rencana ulang dengan memecah tonggak yang belum selesai menjadi teorema-teorema lebih kecil yang dirumuskan secara tepat. Setiap penguraian harus menunjukkan bagaimana bagian-bagian tersebut dapat membuktikan tonggak semula melalui bukti Lean yang singkat.

Kesenjangan yang Ditemukan dalam Bukti Terbitan

Penerjemahan bukti ke Lean mengungkap masalah dalam argumen yang telah diterbitkan, menurut laporan Axiom. Sebagian besar masalahnya kecil—kesalahan ketik, kesalahan dalam tabel, atau hipotesis yang terlewat—tetapi perusahaan tersebut mencatat 34 penyimpangan penting dari naskah yang diterbitkan. Penyimpangan yang paling besar berkaitan dengan Unbalanced Group Theorem, atau UGT.

Salah satu contohnya ditemukan dalam jilid-jilid kuasipipis karya Aschbacher dan Smith, yang memuat sebuah lemma yang menyatakan bahwa dua besaran numerik sama. Para agen menemukan contoh penyangkal yang melibatkan grup SL₂(5), dengan salah satu besaran bernilai 1, padahal kesamaan yang dinyatakan mengharuskannya bernilai 2. Mengganti kesamaan itu dengan pertidaksamaan memperbaiki lemma tersebut, tetapi argumen-argumen selanjutnya menggunakan kesamaan itu untuk menyingkirkan sejumlah kasus. Karena itu, tim memperluas argumen sebelumnya agar mencakup konfigurasi-konfigurasi tersebut.

UGT membantu mengidentifikasi suatu grup secara keseluruhan berdasarkan informasi tentang subgrupnya: menurut abstrak makalah yang menyertainya, di bawah hipotesis induktif klasifikasi tersebut, keberadaan subgrup berorde ganjil nontrivial yang normal di dalam sentralisator suatu involusi mengharuskan grup sederhana yang menaunginya bertipe Lie dalam karakteristik ganjil atau berupa grup alternating dengan derajat tertentu. Axiom mengkaji UGT melalui monograf John Walter tahun 1986. Saat memformalkan argumen tersebut, para agennya menemukan contoh penyangkal eksplisit terhadap suatu pernyataan tentang ketertutupan yang digunakan dalam argumen itu: suatu operasi yang diasumsikan mempertahankan grup-grup sederhana terkait di dalam keluarga tertentu ternyata dapat menghasilkan grup yang secara eksplisit dikecualikan dari keluarga tersebut.

Menurut uraian perusahaan, jika dimulai dari PSL₂(49), yang involusi medaninya memiliki sentralisator PGL₂(7), operasi tersebut menghasilkan komponen sederhana PSL₂(7). Grup ini dikecualikan dari keluarga itu karena 7 adalah bilangan prima Mersenne. Axiom mencatat bahwa contoh-contoh penyangkal tersebut tidak membantah UGT itu sendiri, bahkan tidak membantah kesimpulan Proposisi II.5.9(ii) karya Walter.

Perbaikan tersebut bertumpu pada teori Solomon tahun 1976 tentang 2-komponen maksimal, yang menurut Axiom memberikan gagasan-gagasan utama bagi argumen alternatif yang dihasilkan dan diformalkan oleh sistem AxiomProver. Langkah kuncinya, yang dinyatakan dalam makalah sebagai Teorema 2.3 (pelestarian puncak sederhana), disebut Axiom sebagai hasil baru dalam teori grup yang dibuktikan oleh AxiomProver. Jika digabungkan dengan reduksi Gilman dan Solomon serta teorema pengenalan Foote dan Harris, langkah ini menghasilkan bentuk grup sederhana UGT yang diperlukan untuk klasifikasi tersebut. Setelah formalisasi selesai, para matematikawan Axiom menemukan deduksi yang lebih singkat dengan metode generasi pertama, yang dicatat sebagai Catatan 9.5 dan mencapai kesimpulan yang sama tanpa Teorema 2.3.

Makalah tersebut, The Unbalanced Group Theorem, yang disumbangkan oleh Colin Defant dan Ken Ono, diterbitkan di peladen pracetak Hexagon sebagai versi 1 pada 27 Oktober 2026 dengan lisensi CC BY 4.0; halaman proyek mencantumkan panjangnya sebanyak 35 halaman. Axiom menyatakan bahwa perusahaan itu bekerja sama dengan para ahli teori grup untuk menghimpun errata yang ditemukan dalam literatur dan akan menerbitkannya di halaman errata proyek tersebut. Lyons dan Solomon, yang karyanya menjadi landasan klasifikasi itu, dimintai pendapat mengenai perbaikan UGT. Perusahaan tersebut menyatakan akan terus menghimpun dan menyelesaikan errata bersama dewan penasihat yang mencakup keduanya, serta penasihat eksternal Dan Nakano. Axiom menggambarkan kontribusinya sebagai upaya membuat bukti dapat diperiksa secara mekanis, mendokumentasikan kendala yang ditemui, dan menyediakan argumen formal untuk mengatasinya, sembari menyatakan bahwa pencapaian klasifikasi tersebut tetap merupakan hasil kerja para matematikawan yang menemukan grup-grup itu dan mengembangkan argumennya.