Anthropic: Claude har skrivit det första datorverifierade beviset för Fermats sista sats

Anthropic meddelade på torsdagen att deras AI-modell Claude har slutfört det första kompletta, datorverifierade beviset för Fermats sista sats, ett av matematikens mest berömda resultat. Genom att arbeta i stort sett autonomt under 11 dagar skrev Claude beviset i programmeringsspråket Lean, vilket resulterade i 13 miljoner rader kod och 29 500 mellanliggande satser.anthropic+1

En 11 dagar lång spurt genom århundraden av matematik

Fermats sista sats anger att inga positiva heltal a, b och c uppfyller ekvationen aⁿ + bⁿ = cⁿ för något heltal n större än 2. Satsen föreslogs först av Pierre de Fermat omkring 1637 och bevisades inte förrän 1995, då Andrew Wiles publicerade ett 129 sidor långt bevis som krävde månader av expertgranskning för att verifieras.anthropic

Att formalisera beviset, det vill säga skriva om det så att en dator kan kontrollera varje logiskt steg, förväntades ta år. Kevin Buzzard, matematiker vid Imperial College London som lett ett oberoende arbete för att formalisera FLT med hjälp av Lean, bekräftade att koden kompilerar och stämmer. I ett blogginlägg på fredagen kallade Buzzard det en extraordinär prestation inom autoformalisering och noterade att beviset är flerskiktat och spänner över algebra, harmonisk analys, geometri och talteori.xenaproject.wordpress+1

Claudes bevis följer Darmon-Diamond-Taylor-framställningen av Wiles-Taylor-Wiles-argumentet, en förenklad version av det ursprungliga beviset. Mänsklig input begränsades till sporadiska instruktioner på hög nivå från Anthropic-forskaren Tianyi Peng, vars team vid Columbia University byggde Prove2Me-plattformen som möjliggjorde arbetet.anthropic+1

Hur beviset byggdes

Flera tidiga försök misslyckades då Claudes agenter tappade kontrollen över projektets status och slutade samarbeta effektivt. Genombrottet kom när teamet bytte till Prove2Me, en öppen samarbetsplattform som upprätthåller en riktad graf av satsutsagor, vilket tillåter flera agenter att arbeta parallellt och besluta vilka bevis som ska testas härnäst. Genom att använda ett Claude Code-baserat multi-agent-system konsumerade dussintals agenter ungefär sex miljarder utdata-tokens från en intern forskningsmodell som Anthropic beskriver som ungefär jämförbar med Claude Fable 5.1.siliconangle+1

Det färdiga beviset verifierades av Lean med hjälp av endast dess tre standardaxiom, och en komparator bekräftade att satsutsagan stämmer överens med Mathlibs egen formulering av FLT. Med 13 miljoner rader är det över fem gånger så stort som Mathlib, det främsta biblioteket för formaliserad matematik.anthropic+1

Vad det innebär för matematiken

Buzzard, som ursprungligen fick e-post om resultatet medan han var på en musikfestival och avfärdade avsändaren som en tok, skrev att prestationen signalerar en ny era: Om automatisk formalisering av FLT är möjlig nu, har vi tagit ett stort steg mot automatisk formalisering av modern matematisk litteratur. Han noterade att sådana tekniker kan rensa bort fel i den befintliga matematiska litteraturen och lätta på arbetsbördan för granskare som bedömer nya arbeten.anthropic+1

Milstolpen följer en rad AI-drivna framsteg inom matematiken. Anthropic använde Claude förra månaden för att upptäcka ny information om Riemanns zeta-funktion, medan rivalen OpenAI använde sin senaste modell för att lösa flera Erdős-problem. Anthropic använde även nyligen Claude för att motbevisa Jacobian-förmodan i tre dimensioner och uppåt. Buzzard, för sin del, kom med en karaktäristiskt torr kommentar: Jag fick 1 miljon pund för att driva mitt projekt under 5 år; Anthropic tog bara 11 dagar, men jag undrar om de spenderade mer pengar.xenaproject.wordpress+2