Axiom Math, perusahaan sing berbasis ing San Francisco sing mbangun sistem AI kanggo matématika, wis ngrilis bukti lengkap pisanan sing dipriksa komputer saka Klasifikasi Grup Sederhana Terakhir (CFSG), sing digambarake minangka bukti paling dawa ing sajarah matematika. Miturut woro-woro perusahaan, insinyur lan matématikawan ngarahake puluhan agen AI sajrone mung 24 dina kanggo ngasilake kira-kira 43,1 yuta baris kode ing asisten bukti Lean, verifikasi asil sing sadurunge mbentang kira-kira 15.000 kaca ing luwih saka 500 artikel jurnal sing ditulis dening udakara 100 taun.
Prestasi kasebut tekan nalika matematika sing dibantu mesin nyepetake kanthi cepet, lan outlet nelusuri kabar riset AI wis nonton verifikasi resmi pindhah saka praktik khusus menyang kemampuan wates. Sing nggawe rilis iki ora umum yaiku skala: formalisasi kasebut ngemot kira-kira 2,05 yuta deklarasi sing diatur dadi 100 tonggak sejarah, saben siji dicenthang dening kernel Lean, inti cilik sing dipercaya sing verifikasi saben langkah logis.
Apa Sejatine Klasifikasi
Klompok prasaja winates minangka blok bangunan simetri sing ora bisa dipisahake, lan klasifikasi kasebut - dijuluki "teorema gedhe banget" - menehi dhaptar lengkap. Miturut dokumentasi proyek, saben klompok prasaja winates minangka salah siji saka patang jinis: klompok cyclic urutan prima, klompok gantian ing paling limang simbol, siji saka nembelas kulawarga tanpa wates saka klompok jinis Lie dibangun liwat kothak winates, utawa salah siji saka persis 26 kelompok sporadis sing pas karo kulawarga.
Mbuktekaken sing dhaftar iki exhausts saben kamungkinan njupuk bagean luwih saka abad gaweyan bebarengan. John Thompson, sing kerjane dadi pusat klasifikasi kasebut, nampa Medali Fields ing 1970 lan Bebungah Abel ing 2008. Bukti kasebut dawa banget lan disebarake ing kertas lan generasi matématikawan sing isih ragu-ragu babagan kelengkapane nganti pirang-pirang dekade - keraguan formalisasi iki saiki wis dibuwang sacara resmi.
Grombolan Agen Saka 500 Sumber
Bukti asli kasebar ing luwih saka 500 artikel lan buku, pirang-pirang dekade kepungkur ditulis ing notasi sing ora cocog. Insinyur Axiom njlèntrèhaké cara kasebut ing diskusi Hacker News babagan rilis: grombolan agen ditugasi ngliwati kabeh sumber kasebut, kanthi bagean sing angel ngumpulake kabeh dadi sakabehe sing koheren, amarga konsep informal sing padha bisa diresmikake kanthi cara sing rada beda nanging ora cocog sacara matematis.
Kiriman blog perusahaan kasebut nyatakake manawa upaya kasebut butuh 24 dina wiwit diluncurake, kanthi insinyur manungsa lan matématikawan sing ngarahake swarms agen tinimbang nggarap baris demi baris. Asil kasebut ngetutake tonggak formalisasi otomatis kanthi profil dhuwur ing taun 2026, kalebu bukti Lean saka teorema klasik utama sing diprodhuksi nganggo model perbatasan, nanging ing skala ora ana proyek sadurunge.
34 Penyimpangan Saka Rekam sing Diterbitake
Nerjemahake bukti sing diterbitake menyang wangun sing bisa dipriksa mesin mbukak masalah nyata ing literatur matematika. Axiom nglaporake manawa umume masalah cilik - kesalahan tipografi, kesalahan ing tabel, utawa hipotesis sing ilang. Nanging ana 34 panyimpangan sing penting saka cathetan sing diterbitake sing kudu dirampungake sadurunge formalisasi bakal ditindakake.
Sing paling penting yaiku Teorema Kelompok Ora Imbang. Nalika resmi rute generasi pisanan kanggo asil, tim nemokake counterexamples kanggo pratelan penutupan digunakake ing bantahan diterbitake. Ing rembugan karo ahli teori klompok ahli, padha mbangun rute alternatif dibangun ing teknik struktural jaman Daniel Gorenstein - khusus teori 2-komponen maksimal saka taun 1970-an - lan nerbitaké fix minangka kertas teori klompok 35-kaca anyar, dikirim minangka preprint 2610.00575. Perusahaan ngandika bakal nerbitaké dhaftar errata dhowo kanggo entuk manfaat saka masyarakat matématika, nyawiji ing rembugan karo teori klompok ing kang karya klasifikasi dumunung.
Apa Matématika Dipriksa Mesin Penting
Nilai formalisasi ora mung yen komputer nyetujoni bukti kasebut. Formalisasi Lean nyuda basis kepercayaan menyang kernel asisten bukti - program cilik sing diaudit banget - tinimbang kapercayan akumulasi ewu kaca sing diwaca dening spesialis sing kasebar. Komentator ing thread Hacker News, ngendi crita narik kawigaten atusan upvotes, nyathet yen kawruh empiris kenapa klasifikasi kasebut ana ing risiko mati amarga generasi asli matématikawan pensiun, amarga ora ana wong siji-sijia sing bisa nyekel kabeh argumentasi ing sirahe.
Ana gema praktis ing papan liya ing fisika uga. Paling gedhé saka 26 kelompok sporadis, grup Monster, katon ing program "monstrous moonshine" nyambungake simetri finite kanggo fungsi modular - karya sing entuk Richard Borcherds Fields Medal ing 1998 - lan ing proposal Edward Witten 2007 ngubungake simetri Monster menyang entropi universe telung dimensi ing bolongan ireng. Klasifikasi sing wis diverifikasi ndadekake matématika struktural sing ndasari ing dhasar sing luwih kuat kanggo aplikasi lintas disiplin iki.
Apa Sabanjure
Axiom ujar manawa luwih akeh makalah sing asale saka formalisasi bakal ditindakake, bebarengan karo proyek sing salah. Kanggo komunitas metode formal, rilis kasebut nyetel pathokan anyar kanggo proyek verifikasi sing diarahake agen bisa nyoba; kanggo matématika, iku ngowahi sprawling, prestasi kolaborasi setengah abad-dawa menyang artefak siji sing komputer bisa mriksa. Klasifikasi kasebut ora mung dipercaya. Saiki, ing pangertèn sing paling harfiah, wis kabukten - lan bukti kasedhiya kanggo sapa waé sing bisa didownload lan diverifikasi.
