Lean prihvatio Claudeov dokaz Fermatova teorema

Lean, program kojim matematičari diljem svijeta računalno provjeravaju dokaze, prihvatio je potpunu formalnu verziju posljednjega Fermatova teorema. Formalizacija koju je izradio Anthropicov sustav Claude i objavio u otvorenom repozitoriju nema neriješenih koraka, dodatnih aksioma ni računalnih prečaca izvan standardnih temelja Leana (repozitorij). Kevin Buzzard, matematičar s Imperial College London koji je vodio vlastiti projekt formalizacije, neovisno je preveo projekt u izvršivi oblik i potvrdio da provjera prolazi, nazvavši rezultat „izvanrednim postignućem u automatiziranoj formalizaciji” (Buzzard).

Sama je matematika riješena prije više od tri desetljeća. Andrew Wiles dokazao je teorem 1995. i među ozbiljnim matematičarima nije bilo dvojbe o njegovoj valjanosti. Nedostajao je prijevod tog dokaza u upute za doslovan računalni provjerivač, kojemu se moraju zadati svaka definicija i svaki međukorak koji matematičar u pisanom dokazu može podrazumijevati. Prema Anthropicu, deseci agenata umjetne inteligencije obavili su taj posao tijekom jedanaest dana u kolovozu, radeći usporedno na platformi Prove2Me (Anthropic).

No navedeni rok opisuje postupak koji vanjski istraživači ne mogu ponoviti. Anthropic nije objavio interni model, infrastrukturu za koordinaciju agenata, odluke operatera ni utrošene računalne resurse. Ponovljivo je samo konačno djelo: svatko s dovoljno snažnom opremom može ponovno prevesti projekt u Leanu i potvrditi da dokaz prolazi provjeru. Zaseban provjerivač koji je Anthropic napisao u Rustu potvrdio je isti formalni zapis i dosljednost svih 1.052.234 deklaracija (tehničko izvješće). Riječ je, međutim, o drugom čitanju istoga teksta, a ne o neovisnom ponavljanju jedanaestodnevnog postupka njegova nastanka.

Kako su agenti radili

Formalizirati dokaz znači preoblikovati matematički argument tako da program bez matematičke intuicije može potvrditi svaki logički korak. Sam teorem zvuči jednostavno: ni za jedan cjelobrojni eksponent jednak ili veći od tri ne postoje tri pozitivna cijela broja koja zadovoljavaju jednadžbu aⁿ + bⁿ = cⁿ. Dokaz se, međutim, proteže na stotinama stranica i oslanja na duboke rezultate iz više područja teorije brojeva.

Claude nije otkrio novu matematiku, nego je formalizirao poznati niz rezultata koji vodi do Wilesova dokaza, oslanjajući se na prikaz matematičara Henrija Darmona, Freda Diamonda i Richarda Taylora (Anthropic, tehničko izvješće). Stvaralački matematički uvid pripada Wilesu i njegovim prethodnicima. Claudeov je doprinos prijevod tog znanja u približno 10,5 milijuna redaka računalno provjerljivog programskog koda (tehničko izvješće).

Platforma Prove2Me, koju su razvili Anthropicov istraživač Tianyi Peng i suradnici sa Sveučilišta Columbia, podijelila je dokaz u graf ovisnosti s približno 29.511 samostalnih tvrdnji (tehničko izvješće). Agenti su preuzimali tvrdnje za koje su preduvjeti već bili riješeni, pisali njihove dokaze u Leanu te međusobno provjeravali predložene formulacije, što je omogućilo usporedan rad. Za cijeli je pothvat interni istraživački model proizveo približno šest milijardi izlaznih tokena (tehničko izvješće).

Prema navodima Anthropica, ljudski operateri tijekom provedbe nisu napisali nijedan redak u Leanu, ali su odabrali teorem, zadali poznati put dokazivanja, osmislili infrastrukturu agenata i povremeno mijenjali prioritete (Anthropic). Cjelovit zapis njihovih uputa i odluka, kao ni troškovi računalne obrade, nisu objavljeni.

Rezultat počiva na godinama ljudskog rada

Formalizacija se oslonila na Mathlib, veliku knjižnicu formalizirane matematike koju održava zajednica, te neposredno preuzela dijelove dvaju ranijih projekata. Buzzardov tim na Imperialu radio je na formalizaciji posljednjega Fermatova teorema u Leanu od kraja 2023., uz milijun britanskih funta potpore britanskog vijeća EPSRC za projekt planiran do 2029. (potpora EPSRC-a). Drugi projekt zajednice već je formalizirao teorem za dio slučajeva. Anthropic u datoteci s podacima o podrijetlu materijala navodi 106 datoteka koje sadržavaju građu preuzetu ili prilagođenu iz tih dvaju pothvata (podaci o autorstvu).

Zbog usporednog rada agenata jedanaest kalendarskih dana ne može se izravno usporediti s brojem radnih sati Buzzardova tima, čiji je projekt do početka Claudeove kampanje trajao približno 22 mjeseca financiranja (potpora EPSRC-a). Anthropic nije objavio ni broj sati rada grafičkih procesora ni potrošnju energije.

Prije ove objave posljednji Fermatov teorem bio je jedina preostala stavka na popisu Freeka Wiedijka sa 100 važnih teorema koje je trebalo formalizirati. Taj se popis već dva desetljeća upotrebljava kao mjerilo napretka u tom području (Buzzard).

Prava provjera primjenjivosti ovoga pristupa bit će formalizacija novije i slabije dokumentirane matematike, za koju ne postoje razrađen plan dokaza, zrele knjižnice ni prethodni formalni radovi. Ovaj je pothvat obuhvatio slavan teorem za koji je znatan dio infrastrukture već postojao. Pokazao je da agenti umjetne inteligencije, uz poznat put dokazivanja i raniji rad na formalizaciji, mogu proizvesti potpun dokaz koji Lean prihvaća, a vanjski stručnjaci mogu ponovno provjeriti. Na temelju objavljenih materijala ipak nije moguće ponoviti sam postupak kojim je formalizacija nastala.