Axiom menyebut agen AI memformalkan Klasifikasi Grup Sederhana Hingga dalam Lean

Axiom, perusahaan AI di bidang matematika, mengumumkan di X bahwa mereka telah menyelesaikan formalisasi otomatis Klasifikasi Grup Sederhana Hingga dalam Lean. Mereka menyebut hasil ini sebagai "tabel periodik simetri". Axiom menggambarkan bukti aslinya sebagai karya sekitar 15.000 halaman yang ditulis oleh lebih dari 100 matematikawan lintas generasi, dan menyebutnya sebagai bukti matematika terbesar dalam sejarah yang diverifikasi komputer.

Menurut repositori open source Axiom, kawanan agen AI menghasilkan sekitar 43,1 juta baris kode Lean dalam 24 hari, mencakup 715 makalah dan buku, serta menandai 34 penyimpangan dari catatan yang diterbitkan. Unggahan akun berita AI TestingCatalog menambahkan bahwa para agen membagi pekerjaan seperti tim perangkat lunak dan menulis kode lebih cepat daripada kemampuan Lean untuk memeriksanya.

Angka-angka ini berasal dari keterangan Axiom sendiri; pengumuman tersebut tidak menyertakan tinjauan independen atas formalisasi ini. Hingga 28 Oktober, unggahan itu mendapat sekitar 6.200 suka di X.