Claude formaliserede angiveligt Fermats sidste sætning i Lean på 11 dage

Anthropic siger, at Claude har produceret den første komplette, ende-til-ende computerkontrollerede Lean-formalisering af Fermats sidste sætning. Den afgørende skelnen er, at Claude ikke fandt selve beviset for sætningen: Systemet omsatte en etableret moderne bevisvej til et meget stort artefakt, som Lean kan verificere mekanisk. Ifølge Anthropic tog det 11 dage med overvejende autonomt agentarbejde og resulterede i cirka 13 millioner linjer Lean-kode. 215

Hvad blev formaliseret?

Fermats sidste sætning siger, at ligningen (a^n+b^n=c^n), når (n) er mindst 3, ikke har nogen ikke-triviel løsning i naturlige tal. I Mathlibs Lean-formulering betyder det, at enhver løsning må have (a=0), (b=0) eller (c=0). Det svarer til den velkendte formulering om, at der ikke findes løsninger i positive hele tal. 31

Projektet fulgte Darmon–Diamond–Taylor-fremstillingen af Wiles/Taylor–Wiles-strategien i stedet for at opfinde en ny matematisk vej. Det er væsentligt, fordi en formalisering skal indkode langt mere end hovedlinjen i argumentet: definitioner, forudsætninger, hjælpeteoremer og alle de forbindende skridt, som en almindelig matematisk artikel ofte kan udelade. Tidligere arbejde på Imperial Colleges FLT-projekt beskriver også ruten som en moderne variant af Wiles/Taylor–Wiles-beviset. 511

Derfor fyldte beviset 13 millioner linjer

En formel bevisassistent accepterer ikke formuleringer som »det følger af et standardargument«. Hver slutning skal udtrykkes, så systemet kan typekontrollere den, og hvert resultat skal bygge på allerede formaliserede afhængigheder.

Anthropic oplyser, at projektet producerede cirka 30.300 computerverificerede teoremer, hvoraf omtrent 29.500 indgår i den endelige afhængighedskæde. Den færdige udvikling spænder over blandt andet algebra, geometri, harmonisk analyse og talteori. 215

Det forklarer også, hvorfor tallet 11 dage ikke bør læses som om århundreders matematisk arbejde blev erstattet på 11 dage. Anthropic oplyser desuden, at der blev genereret omtrent seks milliarder tokens. Arbejdet omfattede mange kandidatbeviser, Lean-kontroller, fejlrettelser og den tekniske organisering af en meget lang formalisering. 5

Nøglen var koordinering af mange agenter

Det rapporterede resultat byggede på mere end én model, der skulle holde et enormt bevis i hukommelsen. Anthropic siger, at tidligere forsøg gjorde fremskridt, men havde svært ved at fastholde en fælles projekttilstand. Det succesfulde forløb brugte en arbejdsramme baseret på Prove2Me, en platform udviklet til samarbejdende matematisk formalisering. 529

Den centrale organisationsidé er en rettet afhængighedsgraf:

• Knuder repræsenterer udestående definitioner, lemmaer eller teoremer.
• Kanter viser, hvilke resultater et senere resultat afhænger af.
• Agenter kan vælge åbne og nyttige opgaver, bevise dem i Lean og gøre resultatet tilgængeligt for andre agenter.
• Systemet kan dermed arbejde nedefra, fra grundlæggende byggesten, mod den endelige sætning.

Prove2Me beskriver modellen som formalisering af »missioner«, hvor agenter bidrager med genbrugelige formelle beviser. 29 I praksis opdeler grafen én lang og skrøbelig opgave i mange kontrollerbare delopgaver og bevarer samtidig projektets hukommelse uden for den enkelte modelkørsel.

Hvad betyder »computerkontrolleret«?

Anthropic oplyser, at slutprojektet ikke indeholder sorry-pladsholdere – Leans måde at lade en påstand stå som accepteret uden bevis – og at det kun anvender Leans tre standardaksiomer. 5

Det er stærkere end en AI, der blot skriver et overbevisende bevis på almindeligt sprog. Leans kerne kontrollerer, om hvert indkodet skridt følger af systemets logiske regler, aksiomer og importerede afhængigheder. Anthropic oplyser også, at slutpåstanden blev kontrolleret mod Mathlibs etablerede formulering FermatLastTheorem. 531

Men kernekontrollen har en præcis grænse: Den verificerer den formelle påstand, der faktisk er indkodet. Mennesker skal fortsat vurdere, om de formelle definitioner og mellemresultater trofast repræsenterer den tilsigtede uformelle matematik. Uafhængig kompilering af det frigivne artefakt og faglig gennemgang af dets afhængighedskæde er derfor afgørende prøver af den rapporterede bedrift.

Hvorfor Kevin Buzzard kalder det ekstraordinært

Ifølge Anthropics rapport beskrev Kevin Buzzard resultatet som en »extraordinary autoformalization achievement« – en ekstraordinær præstation inden for automatisk formalisering. 21 Betydningen er ikke kun, at agenter kan løse enkelte Lean-opgaver. Påstanden er, at de har samlet en dybt lagdelt og genbrugelig formel udvikling i en skala, som tidligere ville være forventet at kræve års koordineret menneskeligt arbejde.

Hvis den type arbejde kan gentages til en overkommelig pris, kan formalisering hjælpe matematikken på flere måder:

• Mere stringent kontrol: Formelle systemer kan afsløre manglende forudsætninger, ugyldige omskrivninger og uforenelige definitioner, som er svære at opdage i løbende tekst.
• Genbrugelig infrastruktur: Når et lemma først er formaliseret, kan senere projekter importere det og stole på kernekontrollen i stedet for at genskabe alle detaljer.
• Et supplement til fagfællebedømmelse: Maskinkontrollerbare beviser kan mindske byrden ved at validere lange tekniske argumenter, mens matematikere stadig vurderer betydning, relevans og strategi.

Det er mulige gevinster, ikke en automatisk erstatning for matematisk dømmekraft. Et formelt bevis kan være logisk gyldigt og alligevel formalisere den forkerte påstand, og prisen for at skabe et artefakt på 13 millioner linjer er fortsat betydelig.

Den mest rimelige læsning af påstanden

Det rapporterede FLT-resultat er en vigtig målestok for AI-assisteret formalisering, fordi målsætningen allerede var matematisk etableret, og fordi det færdige artefakt er tænkt til at kunne kontrolleres uafhængigt. Det bør ikke fremstilles som om Claude netop har løst Fermats sidste sætning.

Den stærkeste og mest præcise fortolkning er snævrere – men stadig betydningsfuld: Anthropic oplyser, at et koordineret agentsystem oversatte et centralt kendt bevis til en Lean-udvikling i hidtil uset skala ved hjælp af grafbaseret opgaveopdeling og formel verificering som løbende feedback. 21529

De næste afgørende spørgsmål er praktiske: Kan eksterne forskere reproducere bygningen, gennemgå om formaliseringen har den tilsigtede matematiske betydning, genbruge dens komponenter og opnå sammenlignelige resultater på anden avanceret matematik? Svarene vil afgøre, om der er tale om en enkeltstående ingeniørbedrift eller et varigt skift i måden, moderne beviser bygges og kontrolleres på.