Beviset er 350 år gammelt. Kontrollen tok elleve dager.
Anthropic har publisert den første maskinkontrollerte utgaven av Fermats siste sats. Det nye er ikke matematikken. Det er at leseren slipper å stole på noen.
Av H. S. Pettersen · 2 min lesing
Begreper i denne artikkelen
Anthropic publiserte fredag den første komplette maskinkontrollerte utgaven av beviset for Fermats siste sats. Claude jobbet i all hovedsak på egen hånd i elleve dager. Underveis skrev modellen 13 millioner linjer i bevisspråket Lean og beviste 29 500 mellomliggende teoremer.
Ikke ny matematikk
Det nye er ikke satsen. Andrew Wiles beviste den i 1995, på 129 sider, etter at en gjennomgang avdekket et hull han brukte et år på å tette. Det nye er kontrollen. Et bevis skrevet for mennesker hopper over de åpenbare stegene, mens Lean krever hvert eneste av dem. Formaliseringen var ventet å ta år: blåkopien det internasjonale miljøet har jobbet etter siden 2024, ledet av Kevin Buzzard ved Imperial College London, er på 86 sider alene.
Dusinvis av agenter, én graf
Første forsøk mislyktes. Agentene mistet oversikten over prosjektets tilstand og sluttet å samarbeide, og de forkastede forsøkene utgjør rundt sju prosent av linjene i sluttresultatet. Gjennombruddet kom med Prove2Me, en åpen plattform bygget av Anthropic-forskeren Tianyi Peng og kolleger ved Columbia University. Den holder en graf over hvilke teoremer som gjenstår, slik at dusinvis av agenter kan plukke hver sin gren uten å tråkke i hverandre. Regningen var rundt seks milliarder output-tokens fra en intern modell selskapet beskriver som omtrent på nivå med Fable 5.1.
Hvem kontrollerer kontrolløren
Buzzard fikk lese beviset før publisering og kaller det en ekstraordinær prestasjon som hviler på matematikkens aksiomer alene. Han er samtidig den eneste eksterne stemmen Anthropic siterer, i Anthropics egen tekst. Det gjør beviset selv til den viktigste kilden: det ligger åpent på GitHub, det bruker Leans tre standardaksiomer, og en komparator bekrefter at påstanden er identisk med Mathlibs. Anthropic har tidligere lagt fram resultater der leseren måtte stole på selskapets egen beskrivelse. Denne gangen kan hvem som helst kjøre kontrollen selv.
Fermat skrev at margen var for smal. Den er nå 13 millioner linjer bred.
