Agen AI bantu formalisasi Klasifikasi Grup Sederhana Berhingga di Lean

Sebuah tim mempublikasikan formalisasi Lean yang lengkap untuk bukti generasi pertama dari Klasifikasi Grup Sederhana Berhingga (CFSG), salah satu hasil kolaboratif terbesar dalam matematika. Bukti aslinya mencapai ribuan halaman jurnal, ditulis sekitar seratus matematikawan selama beberapa dekade, dan menyatakan bahwa setiap grup sederhana berhingga adalah siklik berorde prima, alternating, bertipe Lie, atau salah satu dari 26 grup sporadik. Formalisasinya mencapai 43,1 juta baris Lean dan 2,05 juta deklarasi, dibangun dari korpus 715 makalah dan buku, dengan setiap langkah logis diperiksa oleh kernel Lean.

Yang membuat ini jadi cerita Kav News adalah cara pengerjaannya. Proyek ini memakai agen AI yang bekerja dari sebuah "Agent Blueprint" awal, jadi ini matematika yang diperiksa mesin dan sebagian besar juga dikerjakan mesin, meski halamannya tidak jelas soal seberapa banyak porsi tulisan para agen. Inti pengerjaan dikreditkan ke kelompok kecil termasuk Dean Cureton, Vasily Ilin, Bhavik Mehta, dan Niels Voss, dengan Letong Hong sebagai principal investigator.

Formalisasi ini melakukan lebih dari sekadar membenarkan hasil yang sudah diketahui. Saat memeriksa argumen, tim menemukan counterexample terhadap satu klaim closure yang dipakai pada salah satu jalur publikasi lewat Unbalanced Group Theorem, sebuah celah nyata di literatur, lalu menulis makalah 35 halaman dengan argumen alternatif berbasis teori komponen-2 maksimal dari Solomon tahun 1976. Situs proyeknya memuat rincian lengkapnya.

Kenapa ini penting

Kalau kamu mengikuti verifikasi formal atau AI untuk matematika, ini satu data konkret soal skala: agen membantu memeriksa bukti yang terlalu besar untuk dipegang satu orang di kepalanya, dan dalam prosesnya menemukan cacat yang terlewat oleh manusia. Itulah argumen untuk formalisasi, disampaikan dengan hasil yang memang penting.