Claude formaliserade Fermats stora sats i Lean på elva dagar

Anthropic uppger att ett system av Claude-agenter har gjort den första kompletta, maskinkontrollerade formaliseringen av Fermats stora sats. Arbetet tog elva dagar och resulterade i 13 miljoner rader Lean-kod. Det betyder inte att Claude hittade ett nytt bevis: agenterna översatte en känd bevisväg till ett format som en dator kan kontrollera steg för steg.

En graf höll agenterna på spåret

Försöken misslyckades först när agenterna tappade projektets tillstånd och slutade samarbeta effektivt. Genombrottet kom med Prove2Me, ett system som organiserade uppgiften som en riktad acyklisk graf. Varje delmål fick ett uttryckligt påstående, ett bevis och beroenden till andra delar.

Systemet skilde dessutom på påståenden och bevis för att korta kompileringstiderna. Naturliga språkbeskrivningar gjorde det lättare för agenterna att hitta och återanvända redan bevisade resultat. Det är en viktig teknisk detalj: den materiella förmågan ligger lika mycket i samordningen och minnet som i den enskilda modellen.

Förenklad rekonstruktion av Prove2Me-flödet. Källa: Anthropic. Grafik: Debrief. Bearbetning: egen faktagrafik utifrån Anthropics tekniska beskrivning; ingen generativ bildmodell använd.

Ett verifierat bevis, inte en ny lösning

Enligt Anthropic samarbetade dussintals agenter med en intern generell forskningsmodell som ungefär motsvarar Claude Fable 5.1. Körningen använde omkring sex miljarder utgående tokens. Agenterna bevisade 30 300 delsatser, varav 29 500 används i slutresultatet.

Formaliseringen följer en förenklad framställning av Andrew Wiles bevis. Lean-kontrollen använder bara systemets tre standardaxiom, och en separat jämförelse kontrollerade att slutsatsen motsvarar Mathlibs formulering av satsen. Matematikern Kevin Buzzard granskade resultatet på Anthropics uppdrag.

Omfattningen är samtidigt en varningssignal. Beviset är mer än fem gånger större än hela Mathlib, det etablerade biblioteket för Lean. Anthropic bedömer att mycket kan kortas och betonar att en mänskligt läsbar framställning fortfarande behövs.

Flaskhalsen flyttar

Formella bevisassistenter kan kontrollera varje logiskt steg, men människor har hittills behövt översätta informell matematik till kod för hand. IEEE Spectrum beskriver just den översättningen som en central flaskhals som språkmodeller börjar angripa.

Det nya här är därför inte att en AI ”löste” ett olöst problem. Det är att ett multiagentsystem höll ihop en redan känd beviskedja i en skala där manuell formalisering är mycket dyr. Om metoden fungerar på fler områden kan forskare lägga mindre tid på att mata bevisassistenter och mer på att formulera hypoteser, hitta luckor och förstå varför ett bevis fungerar.