Lean godkänner Claudes Fermatbevis

Lean, ett program som matematiker världen över använder för att kontrollera bevis, har godkänt en fullständig formell version av Fermats stora sats. Formaliseringen har tagits fram av Anthropics Claude-system och publicerats öppet. Den innehåller inga olösta platshållare, extra axiom eller beräkningsmässiga genvägar utöver Leans standardmässiga grundvalar (repository). Kevin Buzzard, matematiker vid Imperial College London och ledare för ett eget formaliseringsprojekt, har oberoende kompilerat projektet och bekräftat att det klarar kontrollen. Han beskriver resultatet som "en enastående prestation inom automatisk formalisering" (Buzzard).

Matematiken avgjordes för länge sedan. Andrew Wiles bevisade satsen 1995, och resultatet har inte varit ifrågasatt bland seriösa matematiker. Det återstående arbetet bestod i att skriva om beviset till instruktioner för en bokstavligt arbetande kontrollör, där varje definition och mellanled som en matematiker kan lämna underförstått måste anges. Enligt Anthropic slutförde ett tiotal AI-agenter arbetet på elva dagar i augusti. De arbetade parallellt på en plattform kallad Prove2Me (Anthropic).

Tidsuppgiften beskriver dock en process som utomstående inte kan upprepa. Den interna modellen, infrastrukturen för samordning, operatörernas beslut och beräkningskostnaden ingår inte i det offentliggjorda materialet. Slutprodukten går däremot att kontrollera: den som har tillräcklig datorkapacitet kan kompilera Lean-projektet på nytt och bekräfta att beviset godkänns. En separat kontrollör, skriven i Rust av Anthropic, granskade samma formella material och bekräftade att samtliga 1 052 234 deklarationer är konsistenta (technical report). Det är en andra kontroll av samma text, inte en oberoende upprepning av det elva dagar långa arbetet.

Så arbetade agenterna

Att formalisera ett bevis innebär att skriva om matematikerns resonemang så att ett program utan matematisk intuition kan kontrollera varje logiskt steg. Själva satsen är enkel att formulera: för heltalsexponenter på minst tre finns inga tre positiva heltal som uppfyller aⁿ + bⁿ = cⁿ. Beviset går däremot genom avancerad talteori och omfattar hundratals sidor.

Claude upptäckte ingen ny matematik. Systemet formaliserade den etablerade kedja av resultat som leder fram till Wiles bevis och följde en framställning av matematikerna Henri Darmon, Fred Diamond och Richard Taylor (Anthropic, technical report). Den matematiska idén kom från Wiles och hans föregångare. Claudes bidrag var att översätta resonemanget till omkring 10,5 miljoner rader maskinkontrollerbar kod (technical report).

Prove2Me, som utvecklats av Anthropic-forskaren Tianyi Peng tillsammans med forskare vid Columbia University, delade upp beviset i en beroendegraf med omkring 29 511 fristående påståenden (technical report). Agenterna valde påståenden vars förutsättningar redan var klara, skrev Lean-bevis och kontrollerade varandras formuleringar. Därmed kunde många delar behandlas samtidigt. Arbetet förbrukade omkring sex miljarder utmatningstoken från en intern forskningsmodell (technical report).

Enligt Anthropic skrev de mänskliga operatörerna ingen Lean-kod under körningen. De valde däremot satsen, angav den kända bevisvägen, utformade agentinfrastrukturen och justerade emellanåt prioriteringarna (Anthropic). Varken den fullständiga operatörsloggen eller beräkningskostnaderna har offentliggjorts.

Bygger på flera års mänskligt förarbete

Resultatet var beroende av Mathlib, det stora gemenskapsförvaltade biblioteket för formaliserad matematik, och använde direkt material från två tidigare projekt. Buzzards grupp vid Imperial hade sedan slutet av 2023 arbetat med att formalisera Fermats stora sats i Lean. Projektet finansierades med ett anslag på 1 miljon pund från EPSRC och var planerat att pågå till 2029 (EPSRC award). Ett separat gemenskapsprojekt hade redan formaliserat satsen för en delmängd av fallen. Anthropics redovisning anger att 106 filer innehåller material som hämtats eller bearbetats från dessa projekt (attribution).

Eftersom agenterna arbetade parallellt går de elva kalenderdagarna inte att jämföra direkt med den arbetstid som Buzzards grupp lagt ned. När Claude-körningen inleddes hade det finansierade projektet pågått i omkring 22 månader (EPSRC award). Anthropic har inte redovisat antalet GPU-timmar eller energiförbrukningen.

Före publiceringen var Fermats stora sats den sista punkten på Freek Wiedijks lista över 100 betydelsefulla satser som ännu inte hade formaliserats. Listan har använts för att följa utvecklingen inom området i två årtionden (Buzzard).

Ett mer krävande prov blir att formalisera nyare och sämre dokumenterad matematik, där det saknas en etablerad bevisplan, mogna bibliotek och tidigare formaliseringsarbete. Den här körningen gällde en välkänd sats med omfattande infrastruktur på plats. Den visar att AI-agenter kan skapa en fullständig formalisering som Lean godkänner och som utomstående kan kontrollera, förutsatt att de får en känd bevisväg och tillgång till tidigare formellt arbete. Hur själva arbetet genomfördes går fortfarande inte att återskapa med det publicerade materialet.