Klasifikasi Grup Sederhana Berhingga (CFSG) dalam matematika modern merupakan salah satu proyek pembuktian yang paling besar skalanya.
Pembuktian ini, yang diselesaikan secara berantai oleh ratusan matematikawan selama puluhan tahun, hasilnya tersebar di ratusan makalah dan monograf, dengan total halaman mendekati dua puluh ribu halaman. Skalanya jauh melampaui batas yang dapat ditinjau ulang secara lengkap oleh satu orang atau bahkan satu tim.
Dalam konteks ini, memperkenalkan AI untuk membantu verifikasi formal skala besar menjadi jalur baru yang harus dicoba.
Untuk memajukan perkembangan AI for Math, atas dorongan Prof. Shing-Tung Yau, tim peneliti yang terdiri dari siswa Kelas Pemimpin Qiu Zhen dari Universitas Tsinghua, serta Pusat Ilmu Matematika Yau, Institut Riset Industri Cerdas, dan Universitas Warwick, mengusulkan FormaTheoria — Alur Kerja Bantuan Kecerdasan Buatan untuk Penelitian Matematika: membiarkan AI mulai dari literatur matematika asli, secara otomatis merapikan hubungan ketergantungan, mengintegrasikan sistem pengetahuan, membangun pembuktian formal, dan akhirnya menyerahkannya ke pembantu pembuktian Lean untuk verifikasi bertahap.
Hingga Agustus 2026, FormaTheoria telah menyelesaikan formalisasi Lean untuk empat teorema kunci, menghasilkan lebih dari 994 ribu baris teori matematika terkode yang saling terkait. Meskipun masih jauh dari verifikasi lengkap Klasifikasi Grup Sederhana Berhingga, pencapaian ini telah menjadi tonggak penting menuju tujuan akhir tersebut.
CFSG Menyediakan Sistem Dasar untuk Banyak Hasil Matematika Penting
"Klasifikasi Grup Sederhana Berhingga" terdengar sangat abstrak. Secara sederhana, ia seperti "daftar suku cadang dasar" tentang simetri berhingga: struktur simetri berhingga yang kompleks apa pun dapat diurai lapis demi lapis, akhirnya menghasilkan sekumpulan unit dasar yang tidak dapat diuraikan lagi; dan peran CFSG adalah memberi tahu matematikawan unit dasar mana saja yang ada.
Biasanya, penelitian matematika akan terlebih dahulu memecah masalah kompleks menjadi unit-unit dasar ini, kemudian menanganinya satu per satu berdasarkan daftar lengkap yang disediakan CFSG. Oleh karena itu, CFSG menjadi infrastruktur yang dapat dipanggil sewaktu-waktu oleh pembuktian lainnya. Jika "infrastruktur" ini menyembunyikan celah, banyak hasil lanjutan yang dibangun di atas kesimpulan terkaitnya mungkin terpengaruh.
Beberapa tinjauan ahli memberikan bukti kuantitatif untuk penerapan GFSG. American Mathematical Society pada tahun 2018 secara khusus menerbitkan monograf Stephen D. Smith "Applying the Classification of Finite Simple Groups: A User’s Guide", dengan 231 halaman, 10 bab, merangkum skenario penerapan GFSG. Dua bab terakhir dalam daftar isi yang dipublikasikan mencantumkan 14 topik penerapan bernomor, termasuk graf jarak transitif, dugaan Frobenius, algoritma grup permutasi, pertumbuhan subgrup grup terhingga yang dihasilkan, perluasan medan, liputan permukaan Riemann, masalah Waring dalam teori grup, graf ekspander dan grup perkiraan.
Nilai penerapan GFSG juga mendapat pengakuan dari tingkat tertinggi komunitas matematika internasional. Kongres Matematikawan Internasional 2014 mengundang pemenang Penghargaan Aljabar Cole 2018 American Mathematical Society, Robert Guralnick, untuk memberikan presentasi khusus berjudul "Applications of the Classification of Finite Simple Groups".
Penerapan ini mencakup hasil penting dengan pengaruh akademis yang sangat besar. CFSG adalah mata rantai kunci dalam bukti lengkap masalah Burnside terbatas. Efim Zelmanov memenangkan Fields Medal 1994 karena menyelesaikan masalah ini. Monograf Smith juga mencantumkan masalah Waring pada grup sederhana berhingga dan graf ekspander sebagai arah penerapan penting CFSG, dengan makalah perwakilan terkait diterbitkan di "Annals of Mathematics" (masalah Waring; diameter grup sederhana berhingga dan penerapannya). Contoh-contoh ini menunjukkan bahwa CFSG telah mendukung serangkaian pekerjaan penting yang meraih penghargaan akademis puncak dan diterbitkan di jurnal matematika terkemuka.
Dari sudut pandang ini, CFSG telah menjadi sistem dasar yang digunakan berulang kali. Seiring semakin banyaknya hasil turunan yang menumpuk, memverifikasi kebenaran dan kemampuannya untuk ditinjau ulang menjadi semakin penting. Melakukan pemeriksaan mesin yang dapat dilacak dan dapat diulang untuk CFSG memiliki makna yang melampaui teori grup itu sendiri.
Namun, kesulitannya terletak pada fakta bahwa bukti sistem dasar ini berasal dari literatur zaman, penulis, dan kondisi default yang berbeda, seringkali tidak konsisten. Satu kutipan bahkan dapat mengarah ke set literatur lainnya. Dalam sejarahnya, sebuah celah penting dalam pembuktian klasifikasi baru ditambal lebih dari dua puluh tahun kemudian oleh monograf dua volume dengan total 1220 halaman. FormaTheoria tidak hanya perlu memverifikasi langkah-langkah penalaran satu per satu, tetapi juga memeriksa apakah definisi, kondisi, dan kutipan di antara ratusan literatur dapat terhubung dengan lengkap, akhirnya membentuk rantai pembuktian tanpa celah.
Bagaimana AI Memajukan Proyek Pembuktian Super Besar
Banyak sistem AI matematika menghadapi soal yang sudah disiapkan, termasuk soal, definisi, dan alat semua tersedia, AI hanya bertugas mencari pembuktian. Tetapi FormaTheoria berbeda, ia perlu terlebih dahulu membangun kembali dasar matematika di balik soal dari tumpukan literatur yang tersebar, baru kemudian menyelesaikan pembuktian. Pekerjaan ini terutama menghadapi empat kesulitan:
Pertama, sistem awalnya tidak tahu berapa banyak bahan yang perlu dikonsultasikan.
Satu kutipan mungkin mengarah ke makalah lain, yang pada gilirannya mengarah ke lebih banyak pekerjaan prasyarat. Proyek awalnya hanya memiliki 3 sumber utama, selama pembuktian ditemukan 12 sumber lagi; bahan tambahan kemudian mencapai 65.6% dari total halaman yang dikonsultasikan. Metode penanganan FormaTheoria adalah: begitu menemukan kekurangan teorema prasyarat tertentu, ia akan menjeda pembuktian saat ini, mencari dan memformalkan dependensi ini, kemudian kembali ke tugas semula untuk melanjutkan. Hasil yang telah diverifikasi disimpan dalam basis pengetahuan terpadu untuk digunakan kembali oleh pembuktian selanjutnya.
Kedua, literatur yang berbeda sulit digabungkan secara langsung.
Penulis yang berbeda menggunakan definisi, simbol, dan kondisi default yang berbeda. Dua definisi mungkin setara secara matematis, tetapi begitu ditulis ke dalam kode Lean, mungkin tidak kompatibel. FormaTheoria akan berulang kali membandingkan teks asli dan kode yang ada, membangun hubungan konversi yang diperlukan. Secara bersamaan, sistem akan melindungi pernyataan matematika yang telah diverifikasi dan memeriksa apakah setiap perbaikan mempengaruhi pembuktian selanjutnya. Dengan cara ini, beberapa karya dan makalah yang awalnya independen dapat secara bertahap diintegrasikan ke dalam kerangka teori yang sama.
Ketiga, kode yang lolos pemeriksaan mungkin masih salah menafsirkan teks asli.
Lean hanya bertanggung jawab memeriksa apakah logika pembuktian konsisten dan apakah kesimpulan diturunkan dari premis, tetapi tidak dapat menilai apakah kesimpulan ini setia kepada teks asli. AI mungkin melewatkan suatu kondisi, membingungkan "semua" dan "ada", atau bahkan salah mengubah kesimpulan. Untuk itu, FormaTheoria secara khusus menyediakan pos pemeriksaan independen: komponen penerjemah pertama-tama menulis pernyataan Lean, komponen peninjau kemudian memeriksa setiap item terhadap teks asli. Dari 14 bagian literatur yang dianalisis dalam makalah, terjemahan pertama dari 11 bagian dikembalikan untuk diperbaiki. Mekanisme peninjauan independen ini menjadi "asuransi" kedua di luar verifikasi mesin.
Keempat, literatur asli itu sendiri mungkin juga bermasalah.
Dalam literatur lama mungkin ada kesalahan ketik, kondisi yang hilang, atau pernyataan yang ambigu. FormaTheoria akan mempertahankan halaman asli, dan ketika pembuktian selanjutnya menemukan kontradiksi, akan melacak kembali. Jika literatur mendukung koreksi, sistem akan menambahkan kondisi atau membangun hubungan kompatibilitas; jika bukti tidak cukup, sistem akan mencatat masalah dan menyerahkannya kepada profesional matematika untuk dinilai.
Selain itu, proyek ini juga menuntut AI untuk menjaga ritme dalam siklus yang panjang. Satu percakapan tidak dapat menampung tugas lengkap. Untuk itu, FormaTheoria menggunakan "peta pembuktian" yang terus diperbarui untuk mengelola kemajuan: target yang lebih berat dibagi menjadi teorema bantu yang lebih kecil, hasil yang berhasil dikembalikan lapis demi lapis ke teorema utama, rute yang gagal juga dicatat untuk menghindari sistem berulang kali masuk ke jalan buntu yang sama.
Pada strategi paralel, proyek ini juga memiliki desain khusus. Tugas yang saling independen dapat dilanjutkan bersamaan; jika beberapa tugas menemukan hasil prasyarat yang sama, sistem hanya menyelesaikannya sekali, dan mengizinkan tugas lain menggunakannya kembali. Sedangkan konten matematika publik yang mungkin mempengaruhi keseluruhan dimodifikasi satu per satu secara berurutan untuk menghindari konflik. Eksperimen komparatif dalam makalah menunjukkan bahwa cara paralel yang sadar dependensi ini mencapai percepatan 4.2 kali pada tugas yang diuji.
FormaTheoria dengan demikian membentuk rantai kerja lengkap: mencari literatur, melengkapi dependensi, menerjemahkan teks asli, membangun pembuktian, verifikasi mesin, peninjauan independen, menyelesaikan konflik, dan menyerahkan masalah yang tidak pasti kepada profesional matematika. Setiap langkah memiliki tanggung jawab yang jelas dan dapat diverifikasi. Ini justru merupakan desain yang dibuat untuk mengatasi kesulitan yang muncul dalam proyek pembuktian super besar, memberdayakan AI untuk secara bertahap menghubungkan literatur matematika yang tersebar menjadi sistem teori yang dapat diperiksa, dilacak, dan dapat diperluas.
△
Tujuh Bulan, Empat Teorema Kunci, Hampir Sejuta Baris Kode yang Dapat Diverifikasi
Pada 22 Januari 2026, FormaTheoria pertama kali mengirimkan kode. Hingga 2 Agustus 2026, proyek ini telah membuka rantai teori kunci yang membentang ke teorema Bender–Suzuki, dan di tengahnya juga secara berurutan menyelesaikan pembuktian teorema Feit–Thompson (orde ganjil), teorema Z* Glauberman, dan teorema Brauer–Suzuki.
Keempat teorema ini tidak terisolasi satu sama lain. Mereka membentuk rute penting yang saling berhubungan dalam Klasifikasi Grup Sederhana Berhingga, di mana pembuktian teorema berikutnya seringkali dibangun di atas dasar matematika besar yang telah diletakkan oleh teorema sebelumnya.
Snapshot proyek yang menyelesaikan pembuktian di atas meliputi:
- Lebih dari 994 ribu baris kode Lean ;
- Lebih dari 850 file kode ;
- Sistem telah mengonsultasikan 15 buku dan makalah, total 1037 halaman, di mana sekitar dua pertiganya ditemukan secara bertahap selama pembuktian berlangsung.
Tentu saja, jumlah baris kode hanya menunjukkan satu aspek dari skala proyek. Jika menelusuri mundur dengan teorema Bender–Suzuki sebagai titik akhir, proyek ini telah membentuk jaringan pembuktian yang berisi 30298 pernyataan matematika, 186187 hubungan dependensi, dengan rantai dependensi terpanjang mencapai 458 lapisan. Jika konten terkait dari basis pustaka Lean juga dihitung, jaringan ini akan meluas menjadi 74922 pernyataan dan lebih dari 1.44 juta hubungan dependensi. Dapat dikatakan, di balik hampir sejuta baris kode terdapat jaringan pembuktian yang saling terkait dan terhubung erat. Penelitian ini menunjukkan bahwa agen AI kini dapat, dengan kerja sama verifikasi mesin dan peninjauan berlapis, terus memajukan proyek matematika besar dan berjarak jauh.
Proses eksekusi proyek yang sebenarnya juga memiliki karakteristik jarak jauh yang panjang. Eksekusi agen terpanjang yang dicatat dalam makalah berlangsung selama 9.17 hari, di mana sistem melakukan 606 kali kompresi dan pengorganisasian informasi yang terakumulasi, sambil terus mempertahankan target pembuktian saat ini, hasil yang telah diselesaikan, dan masalah yang masih harus diselesaikan. Data ini menunjukkan bahwa manajemen proyek mengelola jaringan pembuktian yang terus berevolusi dan berjarak jauh yang panjang, di mana generasi tunggal atau satu percakapan sama sekali tidak dapat mencakup proses yang begitu kompleks.
Sebelumnya, formalisasi matematika skala besar sangat bergantung pada investasi tenaga manusia, biasanya membutuhkan beberapa peneliti yang berkolaborasi selama bertahun-tahun. Referensi sejarah yang dapat dibandingkan: versi formalisasi Rocq dari teorema Feit–Thompson sebelumnya diselesaikan oleh sekitar 15 orang dalam waktu enam tahun. Sementara FormaTheoria menyelesaikan seluruh konten proyek manual itu dalam tujuh bulan, dan lebih lanjut memperluasnya ke pekerjaan formalisasi teorema kunci lainnya. Tujuh bulan untuk satu tugas agen AI tetap merupakan siklus operasi yang sangat panjang, tetapi dibandingkan dengan formalisasi manual tradisional, intervensi AI secara signifikan memperpendek skala waktu pelaksanaan proyek.
△
Formalisasi Membuat Masalah Tersembunyi dalam Literatur Muncul Satu per Satu
Literatur matematika biasanya ditujukan untuk peneliti yang terbiasa dengan bidang tersebut. Oleh karena itu, penulis sering menghilangkan kondisi yang telah muncul sebelumnya, atau menganggap pembaca dapat mengenali hubungan kesetaraan antara definisi yang berbeda. Beberapa kesalahan ketik atau simbol kecil saat dibaca manusia sering diabaikan atau dikoreksi secara alami. Tetapi FormaTheoria berbeda, ia menerjemahkan literatur baris demi baris ke dalam kode Lean, di mana setiap definisi, setiap kondisi, dan setiap langkah penalaran harus ditulis dengan jelas dan tegas. Persyaratan verifikasi baris demi baris yang ketat inilah yang membuat masalah yang sebelumnya tersembunyi dalam literatur asli menjadi jelas terlihat.
Makalah ini mencatat secara rinci berbagai masalah literatur yang ditemukan oleh proyek, termasuk ketidakkonsistenan definisi untuk konsep yang sama dalam bahan yang berbeda, pernyataan teorema yang menghilangkan kondisi yang diperlukan, kesalahan penempatan kondisi pembagian, bahkan subskrip dalam pembuktian juga terdapat kesalahan. Sebagian dari masalah ini dapat dikoreksi secara otomatis berdasarkan konteks literatur; masalah dengan bukti yang tidak cukup akan diserahkan kepada matematikawan untuk dinilai lebih lanjut.
Satu contoh kasus berasal dari dua bahan tentang teorema orde ganjil. Kedua bahan tersebut mendefinisikan "subgrup maksimal tipe I", tetapi perbedaannya adalah: salah satunya mensyaratkan suatu properti berlaku untuk "setiap struktur komplemen"; yang lain hanya mensyaratkan "ada struktur komplemen" yang memenuhi properti tersebut. Secara formal, yang pertama jelas lebih kuat daripada yang kedua, sehingga dua set definisi tidak dapat langsung dihubungkan. FormaTheoria secara tajam mengidentifikasi perbedaan ini selama proses formalisasi, kemudian dengan bantuan teorema Schur–Zassenhaus, membuktikan bahwa kedua definisi di sini sebenarnya setara, sehingga berhasil membangun jembatan yang menghubungkan kedua literatur.
Kasus lain berasal dari lemma Peterfalvi. Pernyataan formal lemma ini menghilangkan prasyarat "orde suatu grup adalah ganjil", namun pembuktian selanjutnya sebenarnya tidak dapat terlepas dari kondisi ini. Meskipun dalam penerapan lemma di bagian selanjutnya, kondisi ini telah dijamin oleh bagian sebelumnya dan keseluruhan argumen tidak terputus, Lean tidak akan secara otomatis menambahkan informasi latar belakang ini. FormaTheoria, setelah melacak jalur pembuktian dan posisi penggunaan lemma ini, secara otomatis menambahkan kondisi yang hilang ke dalam pernyataan teorema, membuat keseluruhan rantai formalisasi lebih lengkap dan andal.
△
Proyek ini juga menemukan kesalahan literatur yang lebih langsung. Satu definisi menulis objek H yang seharusnya muncul menjadi M, dan dua referensi mempertahankan kesalahan yang sama. Teorema Huppert menempatkan faktor d ke dalam kondisi pembagian yang salah; sistem menemukan contoh tandingan dan menghentikan pembuktian, kemudian menyerahkan masalah kepada matematikawan untuk diperiksa. Kondisi yang benar telah dikonfirmasi secara manual. Satu bagian pembuktian Higman juga menulis penomoran sekelompok vektor basis dari u0 ke um, rentang yang benar seharusnya hingga um−1; kesalahan subskrip ini diidentifikasi dan dikoreksi secara otomatis oleh sistem selama proses pembuktian.
Kasus-kasus ini mencerminkan nilai penting lain dari verifikasi mesin untuk proyek matematika besar. FormaTheoria sambil membangun pembuktian formalisasi, juga melakukan tinjauan granular terhadap literatur asli: ia mencatat di mana masalah muncul, kondisi apa yang diperlukan untuk pembuktian selanjutnya, dasar modifikasi berasal dari literatur mana, dan apakah koreksi mempengaruhi hasil lainnya. Untuk CFSG yang dibangun oleh ratusan bahan yang saling terkait, mekanisme peninjauan yang dapat dilacak ini dapat mengubah detail-detail yang sebelumnya bergantung pada pengalaman pembaca untuk dilengkapi, menjadi dasar matematika yang dapat diperiksa secara jelas.
Harapan ke Depan
FormaTheoria saat ini belum menyelesaikan formalisasi keseluruhan Klasifikasi Grup Sederhana Berhingga, masih ada jalan panjang menuju tujuan akhir. Proyek ini terus dipercepat, bergerak menuju formalisasi lengkap salah satu proyek pembuktian dengan skala terbesar dalam matematika modern. Hasil yang ada menunjukkan bahwa AI kini dapat mempertahankan dan memperluas lingkungan matematika skala besar dalam hitungan bulan, melacak hubungan dependensi kompleks di berbagai literatur, dan membangun sistem teori yang saling terhubung dan memiliki skala objektif di bawah verifikasi ketat. Batas kemampuan AI juga mulai berkembang dari menyelesaikan masalah matematika terisolasi, secara bertahap meluas hingga berpartisipasi dalam konstruksi pengetahuan matematika yang sistematis.
Pekerjaan ini juga akan membentuk infrastruktur matematika yang dapat diperluas dan dapat digunakan kembali secara berkelanjutan. Literatur tradisional hanya dapat memberi tahu pembaca "di mana buktinya ditulis"; kode formalisasi lebih jauh mencatat "apa yang bergantung pada setiap kesimpulan", "bagaimana sumber yang berbeda terhubung", "masalah mana yang telah dikoreksi", dan mengatur definisi, lemma, dan pembuktian yang telah diverifikasi menjadi modul pengetahuan yang dapat langsung dipanggil untuk penelitian selanjutnya. Di masa depan, setelah menambahkan alat penjelasan, pencarian, dan visualisasi, jaringan pengetahuan ini diharapkan dapat membantu peneliti lebih cepat memahami struktur keseluruhan CFSG, menggunakan kembali hasil yang ada, dan bahkan memberikan dukungan kuat bagi matematikawan manusia untuk mengeksplorasi hubungan baru dan menemukan teorema baru.
Tim proyek FormaTheoria berharap mengeksplorasi model kolaborasi manusia-mesin yang berorientasi pada era AI: manusia bertanggung jawab menentukan masalah yang layak diteliti dan membuat penilaian kunci, AI menangani pencarian dan deduksi skala besar, sementara sistem formal memastikan setiap langkah yang diterima dapat diperiksa ulang. Ketika suatu pembuktian menjadi begitu besar sehingga tidak ada individu yang dapat meninjaunya kembali dari awal, cara kombinasi ketiganya ini mungkin akan menjadi jalur baru bagi manusia untuk mengelola pengetahuan matematika skala super besar.
Catatan: Status proyek dan hasil kuantitatif dalam artikel ini berasal dari snapshot saat penyelesaian pada Agustus 2026 seperti yang dijelaskan dalam makalah.
Makalah: https://arxiv.org/abs/2608.10894
Kode: https://github.com/Qiuzhen-CFSG/CFSG
Artikel ini berasal dari akun WeChat "量子位", penulis: Tim FormaTheoria
