Ett bevis som en dator kan kontrollera
Anthropic meddelade den 4 september att en intern forskningsmodell har tagit fram det första beviset av Fermats stora sats som en dator kan kontrollera från början till slut. Formaliseringen omfattar omkring 13 miljoner rader Lean, det bevisverktyg matematiker använder för att tvinga varje steg i ett resonemang till en form som en maskin kan verifiera. Arbetet tog elva dagar, uppger Anthropic.
Fermats stora sats säger att inga tre positiva heltal uppfyller a^n + b^n = c^n för något heltal n större än två. Andrew Wiles bevisade den 1995 i en artikel på ungefär 129 sidor, byggd på maskineri som utvecklats under hela 1900-talet. Att granska ett sådant bevis för hand tar specialister år. Att formalisera det — skriva om varje slutledning så att en dator kan bekräfta att den följer — väntades ta ungefär lika lång tid.
Vad modellen faktiskt gjorde
Systemet var enligt Anthropic en intern forskningsmodell för allmänna ändamål, ungefär jämförbar med Claude Fable 5.1, inte en specialbyggd matematikmotor. Flera dussin agenter arbetade parallellt, genererade omkring sex miljarder tokens och bevisade 30 300 satser, varav 29 500 finns med i slutresultatet. Den mänskliga insatsen begränsades till övergripande styrning.
Anthropic uppger att de första försöken misslyckades helt. Körningen som lyckades byggde på en intern plattform som företaget kallar Prove2Me, som håller reda på vilka satser som beror på vilka och låter många agenter arbeta på olika grenar av samma bevis utan att tappa sammanhanget. Ungefär sju procent av de icke-rutinmässiga raderna i slutfilen kom ur de misslyckade försöken.
Det mänskliga förarbetet under resultatet
Resultatet uppstod inte ur intet. Det följer en förenklad version av Wiles resonemang som lagts fram av Henri Darmon, Fred Diamond och Richard Taylor, och det vilar på Mathlib, det matematikbibliotek som tusentals bidragsgivare byggt i Lean under mer än ett decennium, och på det formaliseringsprojekt Kevin Buzzard driver vid Imperial College London. Buzzard, som granskade resultatet, sammanfattade betydelsen som en fråga om tillförlitlighet: artefakterna är nu robusta nog att bygga vidare på, sade han.
Anthropic pekade själv ut begränsningar. Beviset vilar enbart på Leans tre standardaxiom, och en jämförare bekräftade att påståendet som bevisas stämmer med Mathlibs formulering av satsen — kontrollen som hindrar ett system från att bevisa något som är aningen svagare än vad det utger sig för. Men företaget säger också att beviset sannolikt är betydligt längre än det behöver vara, vilket spelar roll för den som vill återanvända delarna.
Varför formaliseringen är det intressanta
Matematiken har i decennier haft en flaskhals i granskningen: bevis i forskningsfronten är så långa att bara en handfull personer kan granska dem, och fel har överlevt publicering. Formalisering tar bort granskarproblemet, till priset av en enorm mängd tålamodsarbete. Den avvägningen har hållit den ovanlig.
Om den tålamodskrävande halvan kan automatiseras i den här skalan förändras kalkylen. Det sällar sig också till en rad liknande påståenden: Anthropic publicerade i augusti arbete om att Claude tagit fram nya resultat kring Riemanns zetafunktion, och OpenAI har uppgett att modellen Astra löst flera öppna Erdős-problem.
Det som är värt att följa är oberoende återanvändning. En Lean-fil på 13 miljoner rader är verifierbar redan genom sin konstruktion — det är hela poängen med Lean — men värdet för yrkesverksamma matematiker beror på om mellansatserna kan lyftas in i Mathlib och användas på annat håll. Anthropic har inte sagt när, eller om, hela artefakten släpps för det ändamålet.
