Axiom Math, sebuah perusahaan berbasis di San Francisco yang membangun sistem AI untuk matematika, telah merilis bukti lengkap pertama yang diperiksa dengan komputer untuk Klasifikasi Grup Sederhana Hingga (CFSG), yang secara luas digambarkan sebagai bukti terpanjang dalam sejarah matematika. Menurut pengumuman perusahaan, para insinyur dan ahli matematika mengarahkan lusinan agen AI hanya dalam waktu 24 hari untuk menghasilkan sekitar 43,1 juta baris kode dalam asisten bukti Lean, memverifikasi hasil yang sebelumnya mencakup sekitar 15.000 halaman di lebih dari 500 artikel jurnal yang ditulis oleh sekitar 100 ahli matematika selama beberapa dekade.
Pencapaian ini dicapai pada saat matematika berbantuan mesin berkembang pesat, dan outlet yang melacak berita penelitian AI telah menyaksikan verifikasi formal beralih dari praktik khusus ke kemampuan terdepan. Apa yang membuat rilis ini tidak biasa adalah skalanya: formalisasinya berisi sekitar 2,05 juta deklarasi yang disusun dalam 100 pencapaian, yang masing-masing diperiksa oleh kernel Lean, inti kecil tepercaya yang memverifikasi setiap langkah logis.
Apa yang Sebenarnya Dikatakan dalam Klasifikasi
Grup sederhana hingga adalah elemen penyusun simetri hingga yang tidak dapat dibagi lagi, dan klasifikasinya — yang dijuluki "teorema raksasa" — memberikan daftar lengkapnya. Menurut dokumentasi proyek, setiap grup sederhana berhingga adalah salah satu dari empat jenis: grup siklik orde prima, grup bolak-balik pada setidaknya lima simbol, satu dari enam belas keluarga grup tipe Lie yang tak terhingga yang dibangun di atas bidang berhingga, atau salah satu dari tepat 26 grup sporadis yang tidak masuk dalam keluarga.
Membuktikan bahwa daftar ini telah menghilangkan segala kemungkinan memerlukan upaya kolektif selama lebih dari satu abad. John Thompson, yang karyanya sangat penting dalam klasifikasi ini, menerima Fields Medal pada tahun 1970 dan Abel Prize pada tahun 2008. Buktinya sangat panjang dan tersebar di berbagai makalah dan generasi ahli matematika sehingga keraguan yang masih ada tentang kelengkapannya tetap ada selama beberapa dekade - keraguan tentang formalisasi ini sekarang secara resmi hilang.
Kawanan Agen di 500 Sumber
Bukti aslinya tersebar di lebih dari 500 artikel dan buku, banyak yang ditulis beberapa dekade lalu dengan notasi yang tidak sesuai. Seorang insinyur Axiom menggambarkan metode ini dalam diskusi Hacker News mengenai rilis tersebut: segerombolan agen ditugaskan untuk menelusuri semua sumber ini, dengan bagian tersulitnya adalah mengumpulkan semuanya menjadi satu kesatuan yang koheren, karena konsep informal yang sama dapat diformalkan dengan cara yang sedikit berbeda namun secara matematis tidak kompatibel.
Entri blog perusahaan menyatakan bahwa upaya tersebut memakan waktu 24 hari dari awal hingga rilis, dengan insinyur manusia dan ahli matematika mengarahkan kawanan agen daripada bekerja baris demi baris. Hasilnya mengikuti pencapaian formalisasi otomatis penting sebelumnya pada tahun 2026, termasuk pembuktian Lean terhadap teorema klasik utama yang dihasilkan dengan model frontier, namun dalam skala yang belum pernah dicapai oleh proyek sebelumnya.
34 Penyimpangan Dari Catatan yang Diterbitkan
Menerjemahkan bukti yang dipublikasikan ke dalam bentuk yang dapat diperiksa oleh mesin mengungkap masalah nyata dalam literatur matematika. Aksioma melaporkan bahwa sebagian besar masalah bersifat kecil — kesalahan ketik, kesalahan dalam tabel, atau hipotesis yang hilang. Namun terdapat 34 penyimpangan penting dari catatan yang dipublikasikan dan perlu diselesaikan sebelum formalisasi dapat dilaksanakan.
Yang paling substansial berkaitan dengan Teorema Grup Tidak Seimbang. Saat memformalkan jalur generasi pertama menuju hasil, tim menemukan contoh yang berlawanan dengan pernyataan penutupan yang digunakan dalam argumen yang dipublikasikan. Dalam konsultasi dengan ahli teori kelompok ahli, mereka membangun rute alternatif yang dibangun berdasarkan teknik struktur era Daniel Gorenstein — khususnya teori 2 komponen maksimal dari tahun 1970an — dan menerbitkan perbaikan tersebut sebagai makalah teori grup setebal 35 halaman, yang diposting sebagai pracetak 2610.00575. Perusahaan mengatakan akan merilis daftar kesalahan yang panjang untuk kepentingan komunitas matematika, yang disusun melalui konsultasi dengan kelompok ahli teori yang menjadi sandaran pekerjaan klasifikasi tersebut.
Mengapa Matematika yang Diperiksa Mesin Itu Penting
Nilai dari formalisasi bukan hanya sekedar komputer menyetujui buktinya. Formalisasi Lean mengurangi basis kepercayaan pada kernel asisten pembuktian — sebuah program kecil yang banyak diaudit — alih-alih akumulasi kepercayaan ribuan halaman yang dibaca oleh spesialis yang tersebar. Para komentator di thread Hacker News, yang mendapatkan ratusan suara positif, mencatat bahwa pengetahuan empiris tentang alasan klasifikasi ini ada dalam bahaya ketika generasi matematikawan asli pensiun, karena tidak ada satu orang pun yang dapat mengingat seluruh argumen di kepala mereka.
Ada juga kesamaan praktis di tempat lain dalam fisika. Yang terbesar dari 26 kelompok sporadis, kelompok Monster, muncul dalam program "monstrous moonshine" yang menghubungkan simetri terbatas dengan fungsi modular - karya yang membuat Richard Borcherds mendapatkan Fields Medal pada tahun 1998 - dan dalam proposal Edward Witten tahun 2007 yang menghubungkan kesimetrian Monster dengan entropi lubang hitam di alam semesta tiga dimensi yang disederhanakan. Klasifikasi yang terverifikasi menempatkan matematika struktural yang mendasarinya pada landasan yang lebih kuat untuk aplikasi lintas disiplin seperti ini.
Apa yang Terjadi Selanjutnya
Axiom mengatakan lebih banyak makalah yang berasal dari formalisasi sedang dalam proses, bersamaan dengan proyek errata. Bagi komunitas metode formal, rilis ini menetapkan tolok ukur baru mengenai apa yang dapat dilakukan oleh proyek verifikasi yang diarahkan oleh agen; untuk matematika, ia mengubah pencapaian kolaboratif selama setengah abad menjadi satu artefak yang dapat diperiksa oleh komputer mana pun. Klasifikasi tersebut tidak lagi sekedar diyakini. Sekarang, dalam arti yang paling harfiah, sudah terbukti — dan buktinya tersedia untuk diunduh dan diverifikasi oleh siapa saja.
