Claude formaliserer Fermat i Lean: intern modell, ikke produkt

Anthropic publiserte 4. september det de kaller det første komplette, maskinsjekkede beviset for Fermats siste teorem i Lean. Det er autoformalisering av et kjent argument, ikke ny matematikk. Modellen som skrev det, er en intern forskningsmodell «omtrent sammenlignbar med Claude Fable 5.1». Den ligger ikke i API-et dere kjøper.

For CIO og CISO er tre tall mer verdifulle enn «historisk øyeblikk»: 11 dager, rundt 13 millioner linjer Lean, og om lag seks milliarder ut-tokens. Dusinvis av agenter, Claude Code-harness og Prove2Me. Uten stillaset mistet agentene oversikten.

Hva som faktisk ble levert

Pierre de Fermat formulerte påstanden rundt 1637. Andrew Wiles og Richard Taylor publiserte det første korrekte beviset i 1995. Det Anthropic har gjort, er å skrive om et kjent resonnement slik at Leans kjerne kan sjekke hvert steg.

Forsker Tianyi Peng, med gruppe ved Columbia, testet om Claude kunne formalisere FLT. Resultatet: et end-to-end-bevis på 11 dager, i hovedsak autonomt. Underveis skrev systemet 13 millioner linjer Lean og beviste 30 300 mellomteoremer, hvorav 29 500 inngår i sluttbeviset. Beviset er over fem ganger større enn Mathlib.

Argumentet følger Darmon, Diamond og Taylors forenkling fra 1995 av Wiles–Taylor–Wiles, ikke den moderne Khare–Taylor-linjen Kevin Buzzard selv formaliserer. Menneskelig matematikk-input var ifølge Anthropic begrenset til sporadiske høynivåhint fra Peng.

Lean sjekket beviset. Det bruker bare Leans tre standardaksiomer. Verktøyet comparator bekreftet at teoremsetningen matcher Mathlibs egen FermatLastTheorem.

Buzzard, som leder Imperial Colleges FLT-prosjekt, kompilerte kodebasen og kjørte comparator. Den går gjennom. Han kaller det et ekstraordinært autoformaliseringsresultat, og understreker samtidig at det matematisk «forteller oss i praksis ingenting» nytt: argumentet følger tidlig litteratur. Formaliseringen fullfører Freek Wiedijks 20 år gamle liste over 100 formaliseringsutfordringer.

Buzzard peker også på at Anthropics bevis alene dekker de eksponentene Mazur/Eisenstein-delen rekker for, og at FLT for regulære primtall allerede var formalisert. Anthropic skriver at de har tilpasset deler fra Imperial College London FLT-prosjektet og flt-regular. GitHub-repoet er merket som forskningsartefakt, ikke vedlikeholdt, under Apache 2.0.

Stillaset, ikke magien

De første forsøkene feilet. Agentene mistet prosjekttilstanden og sluttet å samarbeide. De mislykkede løpene bidro likevel med rundt 7 prosent av de ikke-boilerplate linjene i sluttbeviset.

Det som virket, var Prove2Me, en åpen plattform Peng og Columbia-samarbeidspartnere har bygget: en DAG over teoremsetninger, splitting av setning og bevis i ulike filer, og søk via naturlig språk. Oppå det: et Claude Code-basert multi-agent-harness.

Det er agentorkestrering, ikke en ny modell-ID. Anthropic sier eksplisitt at tokenene kom fra en intern forskningsmodell, omtrent på nivå med Fable 5.1. Ikke bygg innkjøp, SLA eller «vi har Fermat-Claude» på det.

Et sideeksperiment: tre personlige Claude Max-abonnement formaliserte Vinogradovs treprimtallsteorem på tre dager, via Prove2Me. Det viser at stillas pluss forbrukerabonnement kan bære mindre formaliseringsjobber. Det viser ikke at Max-planen deres nettopp har formalisert Wiles.

Hva det koster, og hva det ikke erstatter

Seks milliarder ut-tokens er et budsjett, ikke en anekdote. Hvis dere priser det som Fable 5.1-liste i API, 50 dollar per million ut-tokens, lander bare ut-siden på om lag 300 000 dollar. Anthropic oppgir ikke intern kost. Buzzard, som har 1 million pund over fem år til sitt EPSRC-prosjekt, spør tørt om Anthropic brukte mer på 11 dager.

Kompilering er heller ikke billig. Buzzard skriver at repoet tar nær 20 ganger så lang tid som Mathlib på en 96-kjerners maskin, og at Lean er treig mellom filer selv med 500 GB RAM.

Dette erstatter ikke menneskelig eksposisjon. Buzzard fortsetter sitt prosjekt fordi Anthropic formaliserte 1995-linjen, ikke den moderne, og fordi han har lovet Mathlib-PR og et dokument mennesker kan lese. Anthropic selv skriver at et formalisert bevis ikke bør erstatte en menneskelig fremstilling.

For styret: dette er et eval-signal om at frontier-agenter kan holde et flerukes forskningsløp når oppgaven har en maskinell orakel, Lean-kjernen. Det er ikke AGI, og det er ikke en sikkerhetsklarert produksjonsagent. Første løp uten DAG mistet tilstanden. Det er den CISO-relevante setningen.

Ikke rull ut «autonom forskning» mot produksjonsdata fordi Fermat ble grønn i Lean. Bruk det som bevis på at verifikasjonssløyfer slår åpne chat-agenter når feil er dyre. Logging, identitet per agent og stoppknapp gjelder fortsatt.

Kilder og medier

Primærkilde: Anthropic, Formalizing Fermat's Last Theorem, https://www.anthropic.com/research/formalizing-fermats-last-theorem

Kevin Buzzard, FLT: Anthropic has beaten me to it, https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/

GitHub, anthropics/fermats-last-theorem, https://github.com/anthropics/fermats-last-theorem

Thumbnail: OpenAI Image 2 / hogby.ai