Lean apstiprina Claude Fermā teorēmas pierādījumu

Matemātiķu plaši izmantotā pierādījumu pārbaudes sistēma Lean ir apstiprinājusi pilnīgu Fermā pēdējās teorēmas formalizāciju. Anthropic sistēmas Claude sagatavotajā un publiski pieejamajā projektā nav neatrisinātu pagaidu soļu, papildu aksiomu vai skaitļošanas paņēmienu ārpus Lean standarta pamatiem (repository). Londonas Impērijas koledžas matemātiķis Kevins Bazards, kurš vadīja pats savu teorēmas formalizācijas projektu, neatkarīgi nokompilēja kodu un apstiprināja, ka pārbaude ir sekmīga. Viņš rezultātu nosauca par „izcilu automātiskās formalizācijas sasniegumu” (Buzzard).

Pati matemātiskā problēma bija atrisināta jau sen. Endrū Vailss teorēmu pierādīja 1995. gadā, un matemātiķu vidū par rezultāta pareizību nopietnu šaubu nebija. Neizdarīts bija kas cits: pierādījums bija jāpārraksta kā instrukciju kopums burtiskai pārbaudes sistēmai, skaidri definējot katru jēdzienu un starpsoli, ko sākotnējā darba autors varēja atstāt nepateiktu. Anthropic vēsta, ka vairāki desmiti mākslīgā intelekta aģentu šo darbu augustā paveikuši 11 dienās, paralēli strādājot platformā Prove2Me (Anthropic).

Tomēr no ārpuses šo 11 dienu procesu atkārtot nevar. Publiskotajos materiālos nav iekšējā modeļa, aģentu koordinēšanas infrastruktūras, operatoru lēmumu un izmantoto skaitļošanas resursu. Atkārtoti pārbaudāms ir gala rezultāts: ikviens, kam pieejama pietiekami jaudīga aparatūra, var nokompilēt Lean projektu un pārliecināties, ka pierādījums iztur pārbaudi. To pašu formālo materiālu pārbaudījusi arī Anthropic izstrādāta atsevišķa sistēma Rust valodā, apstiprinot visu 1 052 234 deklarāciju savstarpējo saderību (technical report). Tā ir viena un tā paša teksta otrreizēja pārbaude, nevis neatkarīga 11 dienu darba procesa atkārtošana.

Kā strādāja aģenti

Pierādījuma formalizēšana nozīmē matemātiķa argumentu pārrakstīt tā, lai katru loģisko soli varētu pārbaudīt programma bez matemātiskas intuīcijas. Teorēmas formulējums ir vienkāršs: ja naturāla skaitļa kāpinātājs ir vismaz trīs, nav tādu triju pozitīvu veselu skaitļu, kas apmierinātu vienādojumu aⁿ + bⁿ = cⁿ. Taču pierādījums aptver simtiem lappušu un balstās vairākos sarežģītos skaitļu teorijas slāņos.

Claude neatklāja jaunu matemātiku. Sistēma formalizēja jau zināmo rezultātu virkni, kas ved līdz Vailsa pierādījumam, izmantojot matemātiķu Anrī Darmona, Freda Daimonda un Ričarda Teilora izklāstu (Anthropic, technical report). Radošais atklājums piederēja Vailsam un viņa priekšgājējiem. Claude paveica citu darbu: pārvērta šo matemātisko ideju virkni aptuveni 10,5 miljonos mašīnpārbaudāma koda rindu (technical report).

Anthropic pētnieka Tjaņji Pena un Columbia University līdzstrādnieku veidotā platforma Prove2Me sadalīja pierādījumu atkarību tīklā ar aptuveni 29 511 patstāvīgi formulētiem apgalvojumiem (technical report). Aģenti izvēlējās risināšanai gatavos apgalvojumus, rakstīja tiem pierādījumus Lean valodā un pārbaudīja citu aģentu piedāvātos formulējumus. Paralēlajā darbā iekšējais pētniecības modelis ģenerēja aptuveni sešus miljardus izvades tokenu (technical report).

Anthropic norāda, ka projekta izpildes laikā cilvēki neesot rakstījuši Lean kodu. Tomēr viņi izraudzījās teorēmu un zināmo pierādījuma ceļu, izveidoja aģentu darba infrastruktūru un atsevišķos gadījumos mainīja uzdevumu prioritātes (Anthropic). Pilns operatoru darbību pieraksts un skaitļošanas izmaksas nav publiskotas.

Rezultāts balstās gadiem ilgā cilvēku darbā

Formalizācija balstījās uz Mathlib — apjomīgu kopienas uzturētu formalizētās matemātikas bibliotēku — un tieši izmantoja divu agrāku projektu iestrādes. Bazarda komanda Imperial College London Fermā pēdējās teorēmas formalizāciju Lean vidē veidoja kopš 2023. gada beigām. Projektam bija piešķirts 1 milj. £ EPSRC finansējums, un darbs bija plānots līdz 2029. gadam (EPSRC award). Cits kopienas projekts jau bija formalizējis teorēmu daļai gadījumu. Anthropic izmantoto materiālu uzskaitījumā minēti 106 faili, kuros pārņemts vai pielāgots šo projektu darbs (attribution).

Aģentu paralēlā darba dēļ 11 kalendārās dienas nevar tieši salīdzināt ar Bazarda komandas ieguldītajām cilvēkstundām. Kad sākās Claude darbs, finansētais projekts bija turpinājies aptuveni 22 mēnešus (EPSRC award). Anthropic nav atklājusi nedz izmantoto grafisko procesoru darbības stundu skaitu, nedz enerģijas patēriņu.

Pirms jaunās formalizācijas Fermā pēdējā teorēma bija vienīgais vēl neatrisinātais punkts Frēka Vēdeika 100 nozīmīgu formalizējamu teorēmu sarakstā, kas jau divdesmit gadus kalpo par nozares progresa mērauklu (Buzzard).

Par metodes vispārināmību varēs spriest pēc mēģinājumiem formalizēt jaunāku un sliktāk dokumentētu matemātiku, kurai nav ne gatava darba plāna, ne nobriedušu bibliotēku, ne agrāku formalizācijas iestrāžu. Šajā reizē aģenti strādāja ar slavenu teorēmu, kurai jau bija izveidota plaša infrastruktūra. Rezultāts apliecina, ka mākslīgā intelekta aģenti, saņemot zināmu pierādījuma ceļu un iepriekš paveiktu formalizācijas darbu, spēj radīt pilnīgu Lean pieņemtu pierādījumu, ko var pārbaudīt arī neatkarīgi lietotāji. Taču no publicētajiem materiāliem pašu ģenerēšanas procesu atkārtot nevar.