Axiom ar MI aģentu palīdzību 24 dienās datorā pārbauda garāko pierādījumu matemātikā

Jaunuzņēmums Axiom Math 26. oktobrī publiskoja, pēc paša vārdiem, pirmo pilnīgo datorā pārbaudīto galīgo vienkāršo grupu klasifikācijas pierādījumu. Šo 20. gadsimta matemātikas teorēmu bieži dēvē par garāko cilvēku uzrakstīto pierādījumu: tas izkaisīts vairāk nekā 500 rakstos ar kopumā aptuveni 15 000 lappusēm, un pie tā strādājuši ap simts matemātiķu.

Darbs prasīja 24 dienas. Axiom inženieri un matemātiķi vadīja vairākus desmitus uzņēmuma MI aģentu AxiomProver, kas pierādījumu pārrakstīja Lean – programmēšanas valodā, kurā katru loģisko soli var automātiski pārbaudīt dators. Rezultāts ir aptuveni 43,1 miljons Lean koda rindu. Projekts sākās 1. oktobrī ar plānu, kas darbu sadalīja 108 posmos un aptuveni 380 mazākos uzdevumos.

Galīgās vienkāršās grupas ir it kā galīgo simetriju „atomi”, no kuriem var salikt jebkuru galīgu grupu. Klasifikācija apgalvo, ka katra šāda grupa pieder pie skaidri aprakstīta saraksta: cikliskās pirmskaitļa kārtas grupas, alternējošās grupas, 16 bezgalīgas Lī tipa grupu saimes un tieši 26 tā sauktās sporādiskās grupas. Par ieguldījumu klasifikācijā Džons Tompsons saņēma Fīldsa medaļu un Ābela prēmiju.

Pārrakstot pierādījumu, atklājās arī nepilnības publicētajos darbos. Lielākā daļa bija sīkas, piemēram, drukas kļūdas un neprecizitātes tabulās, taču Axiom saskaitīja 34 būtiskas atkāpes no publicētā. Nozīmīgākā skāra tā saukto nelīdzsvaroto grupu teorēmu: kādā publicētā argumentā izmantotam apgalvojumam atrasti pretpiemēri, tāpēc uzņēmums izstrādāja alternatīvu ceļu, balstoties uz Ronalda Solomona 1976. gada darbu. Izdevums Xenospectrum uzsver, ka šis atradums neapgāž pašu klasifikāciju, bet gan vienu starpposmu tās pierādījumā.

Kods publicēts GitHub ar atvērtu Apache 2.0 licenci, un Axiom norāda, ka visa projekta pārbaude pēc optimizācijām aizņem mazāk nekā diennakti. Uzņēmums sola kopā ar grupu teorijas speciālistiem publicēt arī pilnu atrasto kļūdu sarakstu. Mākslīgā intelekta jaunumu vietne Neural Brew raksta, ka konsultācijās piedalījušies klasifikācijas līdzautori Ričards Laionss un Ronalds Solomons.

Neatkarīgi pārskatītāji gan vēl nav apstiprinājuši, ka pierādījums pilnībā kompilējas un ka formālais teorēmas formulējums precīzi atbilst tam, ko matemātiķi saprot ar klasifikāciju. Arī apgalvojums par „garākā pierādījuma” pārbaudi pagaidām ir paša uzņēmuma vērtējums.

Notikums iekļaujas plašākā tendencē, kad MI uzņēmumi demonstrē savu modeļu spējas sarežģītos matemātikas uzdevumos. Formāla pārbaude Lean vidē gan atšķiras no parastiem MI apgalvojumiem ar to, ka katru soli var neatkarīgi pārbaudīt jebkurš, kam ir pietiekama skaitļošanas jauda.