Lean sprejel Claudeov Fermatov dokaz

Lean, programsko okolje za preverjanje dokazov, ki ga uporabljajo matematiki po vsem svetu, je sprejel celotno formalizacijo zadnjega Fermatovega izreka. Formalni dokaz je pripravil Anthropicov sistem Claude in ga objavil v odprtem repozitoriju. Ne vsebuje nedokončanih korakov ali dodatnih aksiomov, prav tako ne uporablja računskih bližnjic zunaj standardnih temeljev okolja Lean (repository). Kevin Buzzard, matematik z Imperial College London, ki je vodil lasten projekt formalizacije, je neodvisno prevedel izvorno kodo in potrdil, da Lean dokaz sprejme. Dosežek je označil za »izjemen dosežek avtomatske formalizacije« (Buzzard).

Matematično vprašanje je rešeno že dolgo. Andrew Wiles je izrek dokazal leta 1995 in med resnimi matematiki o pravilnosti rezultata ni bilo dvoma. Odprta je ostala formalizacija: dokaz je bilo treba prepisati v navodila za dobesedni računalniški preverjevalnik ter izrecno navesti vse definicije in vmesne korake, ki jih je avtor prvotnega dokaza lahko izpustil. Po navedbah Anthropic je več deset agentov umetne inteligence avgusta to delo opravilo v enajstih dneh, pri čemer so vzporedno delovali prek platforme Prove2Me (Anthropic).

Te časovnice zunanji raziskovalci ne morejo ponoviti. Anthropic namreč ni objavil notranjega modela, infrastrukture za usklajevanje agentov, odločitev operaterjev niti porabe računalniških virov. Ponovljivo je preverjanje končnega izdelka: vsakdo z dovolj zmogljivo strojno opremo lahko projekt v okolju Lean znova prevede in potrdi veljavnost dokaza. Isti formalni zapis je preveril tudi ločeni Anthropicov preverjevalnik, napisan v jeziku Rust, ki je potrdil skladnost vseh 1.052.234 deklaracij (technical report). Gre za drugo branje istega zapisa, ne za neodvisno ponovitev enajstdnevnega postopka njegovega nastanka.

Kako so delovali agenti

Formalizacija pomeni, da matematikov dokaz prepišemo v obliko, v kateri lahko program brez matematične intuicije preveri vsak logični korak. Izrek je na videz preprost: pri katerem koli celoštevilskem eksponentu, večjem ali enakem tri, ne obstajajo tri pozitivna cela števila, za katera bi veljalo aⁿ + bⁿ = cⁿ. Dokaz pa se na več sto straneh opira na zahtevne plasti teorije števil.

Claude ni odkril nove matematike, temveč je formaliziral že znano verigo rezultatov, ki vodi do Wilesovega dokaza. Pri tem se je oprl na razlago matematikov Henrija Darmona, Freda Diamonda in Richarda Taylorja (Anthropic, technical report). Ustvarjalni matematični preboj je delo Wilesa in njegovih predhodnikov; Claude je njihove ugotovitve pretvoril v približno 10,5 milijona vrstic strojno preverljive kode (technical report).

Platforma Prove2Me, ki so jo zasnovali Anthropicov raziskovalec Tianyi Peng in sodelavci z univerze Columbia, je dokaz razdelila v graf medsebojnih odvisnosti s približno 29.511 samostojnimi trditvami (technical report). Agenti so izbirali trditve, za katere so bili predhodni koraki že končani, zanje pisali dokaze v okolju Lean ter medsebojno preverjali predlagane formulacije. Celotni postopek je porabil približno šest milijard izhodnih žetonov notranjega raziskovalnega modela (technical report).

Po navedbah Anthropic človeški operaterji med izvedbo niso napisali nobene vrstice kode Lean. Izbrali pa so izrek in znano pot do dokaza, zasnovali infrastrukturo agentov ter občasno spreminjali prednostne naloge (Anthropic). Celotnega zapisa njihovih posegov in stroškov računske obdelave podjetje ni razkrilo.

Rezultat temelji na letih človeškega dela

Formalizacija je bila odvisna od Mathlib, obsežne knjižnice formalizirane matematike, ki jo vzdržuje skupnost, ter se je neposredno oprla na dva predhodna projekta. Buzzardova skupina na Imperial College London je formalizacijo zadnjega Fermatovega izreka v okolju Lean razvijala od konca leta 2023, pri čemer je projekt do leta 2029 podprla britanska agencija EPSRC z milijonom funtov (EPSRC award). Ločeni skupnostni projekt je pred tem že formaliziral izrek za del primerov. Anthropic je v datoteki z navedbo virov označil 106 datotek, ki vsebujejo gradivo, prevzeto ali prilagojeno iz obeh projektov (attribution).

Ker so agenti delovali vzporedno, enajstih koledarskih dni ni mogoče neposredno primerjati z delovnimi urami Buzzardove skupine, ki je ob začetku Claudeovega projekta delovala približno 22 mesecev financiranega obdobja (EPSRC award). Anthropic ni razkril niti števila ur delovanja grafičnih procesorjev niti porabe energije.

Pred to objavo je bil zadnji Fermatov izrek še zadnja neformalizirana postavka na seznamu 100 pomembnih izrekov Freeka Wiedijka, merilu, s katerim že dve desetletji spremljajo napredek formalizacije matematike (Buzzard).

Pravi preizkus splošne uporabnosti takšnega pristopa bo formalizacija novejše in slabše dokumentirane matematike, pri kateri ni izdelanega načrta dokaza, zrelih knjižnic ali predhodnega formalnega dela. Tokrat so agenti obravnavali znameniti izrek, za katerega je bila znatna infrastruktura že pripravljena. Rezultat dokazuje, da lahko ob znani poti do dokaza in obstoječih formalnih podlagah izdelajo celovito formalizacijo, ki jo Lean sprejme, zunanji raziskovalci pa jo lahko preverijo. Iz objavljenega gradiva pa še vedno ni mogoče ponoviti postopka, s katerim je dokaz nastal.