Claude formaliserte Fermats siste teorem i Lean på 11 dager

«Vi lærer at KI-genererte autoformaliseringsartefakter nå er robuste nok til å bygge videre på», sier Kevin Buzzard, matematiker ved Imperial College London, om beviset Anthropic publiserte 4. september. Buzzard startet i 2024 fellesskapsdugnaden som skulle formalisere Fermats siste teorem i bevisassistenten Lean, et arbeid som var ventet å ta år. Anthropic-forskeren Tianyi Peng satte i gang Claude for å se hvor langt modellen kom. Den kom helt fram.

Å formalisere et bevis betyr å skrive det om slik at en datamaskin kan kontrollere hvert eneste logiske steg. Der et bevis skrevet for mennesker hopper over det åpenbare, må Lean se alt. Det er grunnen til at oppgaven er så tung: Andrew Wiles' bevis fra 1995 gikk over 129 sider og krevde måneder med kontroll fra andre matematikere, og bare planskissen fellesskapet har brukt for den første fasen av formaliseringen er på 86 sider.

Claude jobbet i stedet som dusinvis av samarbeidende agenter på Prove2Me, en åpen plattform for formalisering utviklet av Peng og kolleger ved Columbia University. Agentene definerte begreper, beviste hjelpeteoremer og brukte dem videre til å ta stadig tyngre påstander. Anthropic oppgir at kjøringen brukte rundt seks milliarder output-tokens fra en intern forskningsmodell omtrent på nivå med Claude Fable 5.1. Menneskelig styring var begrenset til korte hint fra Peng underveis, av typen «Jacobian as a scheme sounds high priority».

«FLT-roten leser PROVED på prove2me klokka 02:00:57Z 18. august. Historisk øyeblikk for denne kampanjen.» — utdrag fra Claudes egen tankelogg, publisert av Anthropic

De første forsøkene mislyktes. Agentene fikk tidlig framgang, men mistet oversikten over prosjektets tilstand og sluttet å samarbeide effektivt. Det arbeidet endte likevel som omtrent sju prosent av de ferdige linjene. Gjennombruddet kom da teamet flyttet koordineringen inn i Prove2Me og kjørte agentene gjennom et oppsett bygget på Claude Code. Det er den delen som er direkte overførbar til alt annet du bygger med agenter: flaskehalsen i lange, parallelle kjøringer er ikke modellens evner, men et delt tilstandslager alle agentene kan lese og skrive til, kombinert med en verifikator som gir hardt ja eller nei på hvert delresultat. Lean er en uvanlig streng kompilator, og nettopp derfor kunne kjøringen gå i to uker uten at feil fikk spre seg.

Beviset er kontrollert av Lean, bruker bare Leans tre standardaksiomer, og en komparator har bekreftet at påstanden som bevises er identisk med Mathlibs egen formulering av teoremet. Hele koden ligger åpent på GitHub. Buzzard peker på at det samme maskineriet kan brukes til å luke ut feil i eksisterende matematisk litteratur og til å kontrollere matematikk som språkmodeller selv produserer, en jobb som i dag er dyr og menneskedrevet.

Det er den egentlige nyheten her. Verifikasjon, ikke ny matematikk, er det Claude leverte, og verifikasjon er det som avgjør om du kan stole på det en agent påstår den har gjort.