Lean priėmė Claude’o Fermat įrodymą

Visame pasaulyje matematikų naudojama įrodymų tikrinimo sistema „Lean“ priėmė visiškai formalizuotą didžiosios Fermat teoremos įrodymą. Anthropic Claude’o parengtoje ir viešoje saugykloje paskelbtoje formalizacijoje neliko neužpildytų tarpinių žingsnių, papildomų aksiomų ar „Lean“ standartinius pagrindus apeinančių skaičiavimo metodų (repository). Londono imperatoriškojo koledžo matematikas Kevinas Buzzardas, iki tol vadovavęs atskiram šios teoremos formalizavimo projektui, savarankiškai sukompiliavo projektą ir patvirtino, kad sistema įrodymą priima. Jis tai pavadino „nepaprastu automatinio formalizavimo laimėjimu“ (Buzzard).

Pati matematinė problema išspręsta seniai: Endrius Vailsas teoremą įrodė 1995 m., o rimtų abejonių dėl rezultato nekilo. Tačiau jo įrodymą dar reikėjo perrašyti kaip nuoseklias instrukcijas pažodžiui logiką tikrinančiai sistemai, apibrėžiant visas sąvokas ir išskleidžiant tarpinius žingsnius, kuriuos matematikas savo tekste gali palikti numanomus. Anthropic teigimu, dešimtys lygiagrečiai per „Prove2Me“ platformą dirbusių DI agentų šią užduotį rugpjūtį atliko per vienuolika dienų (Anthropic).

Vis dėlto paskelbtas terminas apibūdina procesą, kurio išorės tyrėjai negali pakartoti: neviešinami naudotas vidinis modelis, agentų koordinavimo infrastruktūra, operatorių sprendimai ir skaičiavimo išteklių sąnaudos. Pakartotinai patikrinti galima galutinį rezultatą — pakankamai galingą aparatinę įrangą turintis asmuo gali iš naujo sukompiliuoti „Lean“ projektą ir įsitikinti, kad įrodymas priimamas. Tą patį formalųjį tekstą patikrino ir atskira Anthropic sukurta „Rust“ programa, patvirtinusi visų 1 052 234 deklaracijų nuoseklumą (technical report). Tai antras to paties rezultato patikrinimas, o ne nepriklausomai pakartota vienuolikos dienų formalizavimo kampanija.

Kaip dirbo agentai

Formalizuojant įrodymą matematiko argumentai perrašomi taip, kad kiekvieną loginį žingsnį galėtų patvirtinti matematinės intuicijos neturinti programa. Teoremos formuluotė paprasta: kai sveikasis laipsnio rodiklis lygus trims arba didesnis, nėra trijų teigiamų sveikųjų skaičių, tenkinančių lygybę aⁿ + bⁿ = cⁿ. Tačiau pats įrodymas apima šimtus puslapių ir remiasi sudėtingomis skaičių teorijos sritimis.

Claude’as nesukūrė naujos matematikos. Jis formalizavo žinomą rezultatų grandinę, vedančią į Vailso įrodymą, remdamasis matematikų Anri Darmono, Fredo Diamondo ir Richardo Teiloro išdėstymu (Anthropic, technical report). Kūrybinės matematinės įžvalgos priklausė Vailsui ir jo pirmtakams. Claude’o indėlis — jų idėjas perrašyti į maždaug 10,5 mln. eilučių kodą, kurį gali patikrinti kompiuteris (technical report).

Anthropic tyrėjo Tianyi Pengo ir Kolumbijos universiteto bendradarbių sukurta „Prove2Me“ platforma įrodymą išskaidė į priklausomybių grafą, apimantį maždaug 29 511 savarankiškų teiginių (technical report). Agentai rinkosi teiginius, kuriems jau buvo parengti visi būtini ankstesni rezultatai, rašė jų įrodymus „Lean“ kalba ir tikrino vieni kitų suformuluotus teiginius. Per visą procesą vidinis tyrimų modelis sugeneravo apie šešis milijardus išvesties žetonų (technical report).

Anthropic teigimu, vykstant projektui žmonės nerašė „Lean“ kodo, tačiau pasirinko teoremą ir žinomą jos įrodymo kelią, sukūrė agentų infrastruktūrą bei kartais keitė darbų prioritetus (Anthropic). Visas operatorių veiksmų žurnalas ir skaičiavimo išlaidos nepaskelbti.

Rezultatas remiasi ilgus metus trukusiu žmonių darbu

Formalizacija rėmėsi „Mathlib“ — didele bendruomenės prižiūrima formalizuotos matematikos biblioteka — ir tiesiogiai panaudojo dviejų ankstesnių projektų medžiagą. Buzzardo komanda Imperatoriškajame koledže didžiosios Fermat teoremos formalizaciją „Lean“ sistema rengė nuo 2023 m. pabaigos; projektui iki 2029 m. numatyta 1 mln. svarų sterlingų EPSRC dotacija (EPSRC award). Kitas bendruomenės projektas jau buvo formalizavęs daliai atvejų taikomą teoremos versiją. Anthropic autorystės ir panaudotos medžiagos faile nurodyti 106 failai, kuriuose yra iš šių projektų perimto arba pagal juos pritaikyto turinio (attribution).

Dėl lygiagretaus agentų darbo vienuolikos kalendorinių dienų negalima tiesiogiai lyginti su Buzzardo komandos darbo valandomis. Prasidėjus Claude’o projektui, žmonių komanda dotacijos lėšomis jau buvo dirbusi apie 22 mėnesius (EPSRC award). Anthropic neatskleidė nei grafikos procesorių darbo valandų, nei energijos sąnaudų.

Iki šios publikacijos didžioji Fermat teorema buvo paskutinis dar neformalizuotas įrašas Freeko Wiedijko sudarytame 100 svarbių teoremų sąraše, pagal kurį formalizavimo pažanga stebima jau du dešimtmečius (Buzzard).

Ar šį rezultatą galima apibendrinti, geriausiai parodytų naujesnės ir prasčiau dokumentuotos matematikos formalizavimas, kai nėra nei parengto įrodymo plano, nei brandžių bibliotekų, nei ankstesnių formalizavimo darbų. Šiuo atveju pasirinkta garsi teorema, kuriai jau buvo sukurta nemaža dalis reikalingos infrastruktūros. Projektas parodė, kad žinomą įrodymo kelią ir ankstesnius formalizavimo rezultatus gavę DI agentai gali parengti išsamią formalizaciją, kurią priima „Lean“ ir gali iš naujo patikrinti nepriklausomi naudotojai. Tačiau iš paskelbtos medžiagos atkurti paties generavimo proceso kol kas neįmanoma.