Claude skal ha formalisert Fermats siste teorem i Lean på 11 dager

Anthropic sier at Claude har laget den første komplette, ende-til-ende maskinkontrollerte Lean-formaliseringen av Fermats siste teorem. Det avgjørende forbeholdet er at Claude ikke oppdaget et nytt bevis. Systemet skal ha oversatt en etablert, moderne bevisvei til et svært omfattende artefakt som Lean kan kontrollere mekanisk. Anthropic oppgir at arbeidet tok 11 dager med i hovedsak autonom agentkjøring og endte på rundt 13 millioner linjer Lean-kode. 215

Hva som faktisk ble formalisert

Fermats siste teorem sier at ligningen (a^n+b^n=c^n), når (n) er minst 3, ikke har noen ikke-trivielle løsninger i naturlige tall. I Mathlibs Lean-formulering må enhver løsning ha (a=0), (b=0) eller (c=0). Det er ekvivalent med den vanlige formuleringen om at det ikke finnes løsninger i positive heltall. 31

Prosjektet fulgte Darmon–Diamond–Taylor-presentasjonen av Wiles/Taylor–Wiles-strategien, i stedet for å finne på en ny vei gjennom matematikken. Det er viktig fordi en formalisering ikke bare må uttrykke hovedideen i et bevis. Den må også kode definisjoner, forutsetninger, hjelpepåstander og alle overgangene som en vanlig matematisk artikkel ofte lar stå underforstått. Imperial College Londons pågående FLT-prosjekt beskriver også sin tilnærming som en moderne variant av Wiles/Taylor–Wiles-beviset. 511

Hvorfor ble det 13 millioner linjer?

En formell bevisassistent godtar ikke formuleringer som «resten følger ved et standardargument». Hvert slutningsledd må uttrykkes på en form systemet kan typekontrollere, og hvert resultat må hvile på allerede formaliserte avhengigheter.

Anthropic oppgir at prosjektet produserte omtrent 30 300 maskinkontrollerte teoremer, hvorav om lag 29 500 inngår i den endelige avhengighetskjeden. Formaliseringen strekker seg over blant annet algebra, geometri, harmonisk analyse og tallteori. 215

Dermed bør tallet 11 dager ikke leses som om systemet erstattet den lange intellektuelle historien bak Fermats siste teorem på under to uker. Anthropic oppgir også rundt seks milliarder genererte tokens. Innsatsen omfattet mange kandidatbevis, Lean-kontroller, feilrettinger og programvarearbeid for å organisere en langvarig formalisering. 5

Nøkkelen var koordinering mellom mange agenter

Resultatet skal ha vært avhengig av langt mer enn én språkmodell som holder et gigantisk bevis i kontekstvinduet. Anthropic sier tidligere forsøk gjorde framgang, men slet med å bevare felles prosjektstatus. Den vellykkede kjøringen brukte et rammeverk basert på Prove2Me, en plattform for samarbeid om matematisk formalisering. 529

Den sentrale organiseringsideen er en rettet avhengighetsgraf:

• Noder representerer utestående definisjoner, lemmaer eller teoremer.
• Kanter viser hvilke resultater som kreves for senere resultater.
• Agenter kan velge åpne og nyttige deloppgaver, bevise dem i Lean og gjøre resultatene tilgjengelige for andre agenter.
• Systemet kan så arbeide nedenfra og opp, fra grunnleggende komponenter til slutteoremet.

Prove2Me beskriver modellen som formaliseringsoppdrag som agenter kan bidra til med gjenbrukbare, formelle bevis. 29 I praksis gjør grafen én lang og sårbar oppgave om til mange små oppgaver som kan kontrolleres, samtidig som den gir prosjektet et varig arbeidsminne utenfor én enkelt modellkjøring.

Hva «maskinkontrollert» betyr – og ikke betyr

Anthropic oppgir at sluttprosjektet ikke inneholder sorry-plassholdere – Leans måte å godta en påstand uten bevis på – og at det kun bygger på Leans tre standardaksiomer. 5

Dette er vesentlig sterkere enn at en AI skriver et overbevisende bevis i vanlig tekst. Leans kjerne kontrollerer om hvert kodede trinn følger av systemets logiske regler, aksiomer og importerte avhengigheter. Anthropic sier også at det ble kontrollert at sluttuttrykket samsvarer med Mathlibs etablerte formulering FermatLastTheorem. 531

Men kjernekontroll har en presis grense: Den bekrefter den formelle påstanden som faktisk er kodet. Mennesker må fortsatt vurdere om de formelle definisjonene og delpåstandene trofast uttrykker den uformelle matematikken som var ment. Uavhengig kompilering av det publiserte artefaktet og faglig gjennomgang av avhengighetskjeden blir derfor avgjørende prøver av påstanden.

Hvorfor Kevin Buzzard kaller det ekstraordinært

Ifølge Anthropics rapport beskrev matematikeren Kevin Buzzard resultatet som en «extraordinary autoformalization achievement» – en ekstraordinær prestasjon i automatisk formalisering. 21 Betydningen ligger ikke bare i at agenter kan løse enkeltoppgaver i Lean, men i påstanden om at de har bygd en dypt lagdelt og gjenbrukbar formell utvikling i en skala som tidligere var ventet å kreve år med koordinert menneskelig arbeid.

Dersom slikt arbeid blir mulig å gjenta på en rimelig måte, kan formalisering få flere bruksområder i matematikken:

• Strengere kontroll: Formelle systemer kan avdekke manglende forutsetninger, ugyldige transformasjoner og definisjoner som ikke passer sammen – feil som kan være vanskelige å oppdage i prosa.
• Gjenbrukbar infrastruktur: Når et lemma først er formalisert, kan senere prosjekter importere det og stole på kjernekontroll i stedet for å rekonstruere alle detaljer.
• Et supplement til fagfellevurdering: Maskinkontrollerbare bevis kan redusere byrden ved å kontrollere lange tekniske argumenter, mens matematikere fortsatt vurderer mening, relevans og strategi.

Dette er mulige gevinster, ikke en automatisk erstatning for matematisk skjønn. Et formelt bevis kan være logisk gyldig og likevel formalisere feil påstand, og kostnaden ved å lage et artefakt på 13 millioner linjer er fortsatt betydelig.

Den mest nøkterne tolkningen

Den rapporterte FLT-formaliseringen er en viktig målestokk for AI-støttet formalisering fordi målteoremet allerede var etablert, og fordi sluttartefaktet er ment å kunne kontrolleres uavhengig. Den bør ikke omtales som at Claude nylig løste Fermats siste teorem.

Den sterkeste, og mer presise, tolkningen er at Anthropic rapporterer at et koordinert agentsystem oversatte et stort, kjent bevis til en Lean-utvikling i en hittil uvanlig skala. Det ble gjort med grafbasert oppgavedeling og formell verifikasjon som løpende tilbakemelding. 21529

De neste spørsmålene er derfor praktiske: Kan utenforstående forskere gjenskape byggingen, ettergå om formaliseringen uttrykker den tilsiktede matematikken, gjenbruke komponentene og oppnå tilsvarende resultater på annen avansert matematikk? Svarene vil avgjøre om dette var en enkeltstående ingeniørbragd eller et varig skifte i hvordan moderne bevis bygges og kontrolleres.