Så uppges Claude ha gjort Fermats sista sats maskinverifierbar på 11 dagar

Anthropic uppger att Claude har producerat den första kompletta, heltäckande och datorverifierade Lean-formaliseringen av Fermats sista sats. Den avgörande distinktionen är att Claude inte upptäckte ett nytt bevis för satsen. Systemet översatte i stället en etablerad modern bevisväg till ett mycket stort formellt objekt som Lean kan kontrollera mekaniskt. Enligt Anthropic tog arbetet 11 dagar, till stor del med autonomt arbetande agenter, och resulterade i omkring 13 miljoner rader Lean-kod. 215

Vad som faktiskt formaliserades

Fermats sista sats säger att ekvationen (a^n+b^n=c^n), för naturliga tal och en exponent på minst 3, saknar icke-triviala lösningar. I Mathlibs Lean-formulering innebär varje lösning att (a=0), (b=0) eller (c=0). Det är ekvivalent med den välkända formuleringen om positiva heltal. 31

Projektet följde Darmon–Diamond–Taylor-versionen av Wiles/Taylor–Wiles-strategin, snarare än att hitta en ny matematisk väg. Det spelar stor roll: en formalisering måste uttrycka inte bara huvudidén i ett bevis, utan också definitioner, förutsättningar, hjälpsatser och alla övergångar som en vanlig matematisk text ofta lämnar underförstådda. Tidigare arbete i Imperial Colleges FLT-projekt beskriver också sin väg som en modern variant av Wiles/Taylor–Wiles-beviset. 511

Varför behövdes 13 miljoner rader?

En formell bevisassistent accepterar inte formuleringar som ”det följer av ett standardargument”. Varje slutledning måste uttryckas på ett sätt som systemet kan typkontrollera, och varje resultat måste vila på redan formaliserade beroenden.

Anthropic uppger att projektet producerade omkring 30 300 datorverifierade satser, varav cirka 29 500 ingår i den slutliga beroendekedjan. Arbetet spänner över bland annat algebra, geometri, harmonisk analys och talteori. 215

Därför ska siffran 11 dagar inte tolkas som att AI:n ersatte den långa idéhistorien bakom Fermats sista sats på elva dagar. Anthropic uppger också att ungefär sex miljarder token genererades. Arbetet omfattade många kandidatbevis, Lean-kontroller, felrättningar och den tekniska organisering som krävs för en långvarig formalisering. 5

Nyckeln: samordning av många agenter

Det rapporterade resultatet byggde på mer än att en enda modell höll ett jättelikt bevis i minnet. Anthropic skriver att tidigare försök gjorde framsteg men hade svårt att behålla ett gemensamt projekttillstånd. Den lyckade körningen använde en styrmiljö baserad på Prove2Me, en plattform för samarbetsinriktad matematisk formalisering. 529

Kärnan är ett riktat beroendediagram:

• Noder motsvarar återstående definitioner, lemman eller satser.
• Kanter visar vilka resultat som krävs för senare resultat.
• Agenter kan välja öppna och användbara deluppgifter, bevisa dem i Lean och göra artefakterna tillgängliga för andra agenter.
• Systemet kan sedan bygga uppåt, från grundläggande komponenter till den slutliga satsen.

Prove2Me beskriver modellen som att starta formaliseringsuppdrag, eller ”missions”, som agenter kan bidra till med återanvändbara formella bevis. 29 I praktiken gör diagrammet ett långt och skört projekt till många kontrollerbara delproblem, samtidigt som projektspecifikt minne sparas utanför en enskild modellkörning.

Vad betyder ”datorverifierad”?

Anthropic uppger att slutprojektet saknar sorry-platshållare – Leans sätt att tillfälligt acceptera ett påstående utan bevis – och att det bara bygger på Leans tre standardaxiom. 5

Detta är betydligt starkare än att en AI skriver ett övertygande bevis på vanlig svenska eller engelska. Leans kärna kontrollerar om varje kodad slutledning följer av systemets logiska regler, axiom och importerade beroenden. Anthropic uppger också att man verifierat att slutsatsen stämmer överens med Mathlibs etablerade formulering FermatLastTheorem. 531

Men kärnkontrollen har en tydlig gräns: den verifierar det formella påstående som har kodats. Människor behöver fortfarande bedöma om definitionerna och de mellanliggande satserna troget representerar den avsedda informella matematiken. Oberoende kompilering av det publicerade materialet och expertgranskning av beroendekedjan blir därför centrala tester av bedriften.

Varför Kevin Buzzard kallar det extraordinärt

Enligt Anthropics rapport beskrev matematikern Kevin Buzzard resultatet som en ”extraordinary autoformalization achievement” – en extraordinär prestation inom automatisk formalisering. 21 Betydelsen är inte bara att agenter kan lösa enstaka Lean-övningar, utan att de uppges ha satt ihop en djupt skiktad och återanvändbar formell utveckling i en skala som tidigare förväntats kräva många års samordnat mänskligt arbete.

Om metoden går att reproducera och göra ekonomiskt rimlig kan formalisering få flera användningar:

• Striktare kontroll: formella system kan hitta saknade antaganden, ogiltiga steg och definitioner som inte passar ihop – sådant som kan vara svårt att upptäcka i löpande text.
• Återanvändbar infrastruktur: när ett lemma väl är formaliserat kan senare projekt importera det och förlita sig på kärnkontrollen i stället för att bygga om varje detalj.
• Ett komplement till sakkunniggranskning: maskinläsbara bevis kan minska arbetet med att kontrollera långa tekniska argument, medan matematiker fortsatt bedömer innebörd, relevans och strategi.

Det här är möjliga vinster, inte automatiska ersättare för mänskligt omdöme. Ett formellt bevis kan vara logiskt giltigt men ändå formalisera fel påstående, och kostnaden för att skapa en artefakt på 13 miljoner rader är fortfarande betydande.

Den rimliga tolkningen av uppgiften

Det rapporterade FLT-resultatet är ett viktigt riktmärke för AI-stödd formalisering, eftersom målsatsen redan var etablerad och den slutliga artefakten är tänkt att kunna kontrolleras oberoende. Det bör inte beskrivas som att Claude på nytt löste Fermats sista sats.

Den starkaste, och mer precisa, tolkningen är att Anthropic uppger att ett samordnat agentsystem har översatt ett stort känt bevis till Lean i en tidigare osedd skala, med grafbaserad uppdelning av arbetsuppgifter och formell verifiering som återkoppling. 21529

Nästa frågor är praktiska: Kan externa forskare reproducera bygget? Kan de granska att formaliseringen betyder det den avser att betyda? Kan dess delar återanvändas? Och går samma arbetssätt att upprepa för annan avancerad matematik? Svaren avgör om detta är en engångsprestation inom ingenjörskonst eller ett varaktigt skifte i hur moderna bevis byggs och kontrolleras.