Lean bevisassistent och AI: så blir bevis maskinellt kontrollerbara

Elva dagar, en svärm av agenter, 13 miljoner rader kod: En AI har gjort beviset för Fermats sista sats maskinellt kontrollerbart. Avgörande var mindre beräkningskraften än en granskare som inte släpper igenom något fel.

Omkring 1637 antecknade Pierre de Fermat ett påstående i marginalen på en bok och sade sig ha ett bevis för det. Det hittades aldrig. Först 1995 publicerade Andrew Wiles ett fullständigt bevis. Den 4 september 2026 meddelade Anthropic att en svärm av Claude-agenter har formaliserat det beviset fullständigt i bevisspråket Lean. Det blev möjligt tack vare Lean bevisassistent, som kontrollerar varje steg i ett bevis maskinellt.

Den här artikeln placerar meddelandet i sitt sammanhang. Den förklarar vad en bevisassistent är och varför ett resultat från Lean anses tillförlitligt. Den beskriver hur agenterna samarbetade och sätter meddelandet i relation till olympiaduppgifter och Erdős-problem. Belagda siffror, tillverkaruppgifter och öppna frågor hålls isär. Tesen: Det nya är inte bara att en AI arbetar med matematik. Det nya är kombinationen av en modell som får prova fritt och ett program som obönhörligt godkänner eller avvisar varje steg.

Fermats sista sats: vad Anthropic faktiskt har meddelat

Satsen säger att ekvationen aⁿ + bⁿ = cⁿ saknar lösning för heltal större än noll och en exponent n större än 2. Påståendet är lätt att förstå och var extremt svårt att bevisa under århundraden. År 1908 utlystes ett pris på 100 000 guldmark, och enligt Anthropic kom det under det första året in 621 felaktiga bevis. Wiles presenterade ett bevis 1993, hittade en lucka och slöt den tillsammans med Richard Taylor. Publiceringen följde i maj 1995.

Det senaste meddelandet gäller frågan hur säkert beviset är när varje steg kontrolleras av en maskin. De viktigaste uppgifterna ur Anthropics publikation finns i tabellen.

En token är här en liten textbit som en språkmodell genererar, ungefär en ordstam. Några kostnader i pengar nämns inte i källan. Alla uppgifter kommer från tillverkaren och har inte räknats om oberoende i den här formen.

Avgränsningen är viktig. Det rör sig om en formalisering, inte om ett nytt bevis. Satsen var bevisad sedan 1995. Enligt Anthropic byggde agenterna vidare på en förenklad version av Wiles bevis av Darmon, Diamond och Taylor och tog över delar från formaliseringsprojektet vid Imperial College och projektet flt-regular. Den som läser om en AI-lösning av Fermats sats ska alltså inte tänka på en ny matematisk upptäckt, utan på en verifiering. Anthropic skiljer uttryckligen resultatet från AI-arbetet kring Riemannhypotesen, där något nytt uppges ha upptäckts.

Lean bevisassistent: ett verktyg som inte hoppar över något steg

Lean bevisassistent är ett programmeringsspråk med öppen källkod där matematiska bevis kan skrivas ned så att en dator kan kontrollera dem. Projektsidan lean-lang.org beskriver Lean som ett programmeringsspråk och en bevisassistent med en minimal, pålitlig kärna som säkerställer korrektheten. Lean utvecklades av Leonardo de Moura och släpptes som öppen källkod 2013, vilket Simons Foundation rapporterar. Sedan 2023 arbetar den ideella organisationen Lean FRO med vidareutvecklingen, bland annat med stöd av 5 miljoner US-dollar från Simons Foundation International.

Principen går att beskriva med vardagliga ord. Ett bevis i Lean är ett program. Leans kärna kontrollerar steg för steg om varje slutsats följer av axiomen och av redan kontrollerade satser. Axiom är matematikens grundantaganden, som gäller utan bevis. Ett steg som inte följer avvisas, hur övertygande det än låter. Där ett bevis ännu saknas står platshållaren ”sorry” i Lean. Ett bevis med sådana platshållare räknas som ofullständigt.

Just det gör Lean så användbart för AI-modeller. Språkmodeller kan formulera sig övertygande och ändå göra fel. I matematiken är det ett problem, eftersom ett fel i steg 400 kan göra allt som följer värdelöst. Med en bevisassistent som Lean försvinner frågan om modellen går att lita på.

En mänsklig granskning fungerar annorlunda. Experter läser ett bevis, bedömer det som rimligt och förlitar sig på sin erfarenhet. Det är värdefullt, men tar tid och lämnar utrymme för missade fel. Redan 2021 validerade ett gemensamt projekt i Lean ett komplext bevis av Peter Scholze, som Simons Foundation berättar. Bevisassistentens kontroll ersätter inte den matematiska förståelsen, men den ger visshet om korrektheten.

Förloppet i bild 1 visar arbetsfördelningen: Modellen kommer med förslag, Lean-kärnan dömer. Om ett förslag kommer från en människa, en modell eller en slumpgenerator spelar ingen roll för domen.

Mathlib och frågan om vem som kontrollerar det som kontrollerats

Lean i sig innehåller ännu ingen matematik. Den finns i Mathlib, det gemensamt utvecklade biblioteket som nästan alla formaliseringar bygger på. Lean-sidan anger mer än en miljon rader. Communityns statistiksida visade vid avläsningen 139 391 definitioner, 290 502 satser och 772 bidragsgivare. Den som bevisar något i Lean kan använda dessa kontrollerade byggstenar i stället för att börja från noll.

Som jämförelse: Fermat-beviset omfattar enligt Anthropic cirka 13 miljoner rader och är därmed mer än fem gånger så stort som Mathlib. Det låter som en gigantisk nybyggnad, men visar också hur mycket formell verifiering av djupa satser kostar, även när Mathlib utgör grunden. Beviset beror på det som redan är formaliserat i Mathlib.

Två kontrollfrågor måste ställas åtskilda. För det första: Är beviset korrekt? Det besvarar Lean. Anthropic uppger att bara de tre standardaxiomen används. För det andra: Har verkligen Fermats sats bevisats, och inte ett förändrat påstående? Här användes ett comparator-verktyg som bekräftade att det formaliserade påståendet stämmer överens med formuleringen i Mathlib. Den uppdelningen är avgörande. Ett felfritt bevis för ett felaktigt påstående vore värdelöst.

Hela beviset finns enligt Anthropic tillsammans med en skriftlig förklaring på GitHub och kan granskas där. Det som inte är offentligt är bara den modell som användes.

Kevin Buzzard vid Imperial College London, som leder formaliseringsprojektet sedan 2024, granskade beviset. Enligt Anthropic konstaterar han att satsen bevisas utan andra antaganden än matematikens axiom. En gräns återstår: Lean kontrollerar korrekthet, inte betydelse. Om ett resultat är intressant, elegant eller viktigt bedömer verktyget inte. Simons Foundation återger motsvarande bedömningar av Alex Kontorovich.

Agentisk AI: varför svärmen fungerade

Flera dussin agenter arbetade parallellt. En agent är i det här sammanhanget en språkmodell som inte bara svarar utan självständigt använder verktyg, redigerar filer och kontrollerar mellanresultat. Ramverket för flera agenter byggde på Claude Code. Agenterna definierade begrepp, bevisade mellansatser och använde dem för svårare påståenden. En allmän introduktion ger artikeln Das Zeitalter der KI-Agenten.

Genombrottet kom enligt Anthropic inte från en starkare modell utan från bättre organisation. Plattformen Prove2Me, en öppen samarbetsplattform från Tianyi Peng och kollegor vid Columbia University, erbjöd tre egenskaper:

• En riktad acyklisk graf över satspåståendena gav orientering: Varje påstående visar vad det beror på, och det finns inga cykler.
• Påståenden och bevis låg i separata filer. Det påskyndar Lean-kompileringen, eftersom allt inte behöver kontrolleras på nytt vid varje ändring.
• Redan bevisade satser kunde sökas och återanvändas via beskrivningar i naturligt språk.

Tidigare försök utan den här strukturen misslyckades eftersom agenterna tappade bort projektets status. Det är intressant att dessa försök ändå bidrog med cirka 7 procent av de icke-triviala raderna i det slutliga beviset. Lärdomen: Vid stora uppgifter slår struktur den råa modellstyrkan. Den som sätter in många agenter behöver en gemensam plan, delad lagring och tydliga ansvarsområden. Samma erfarenhet gör utvecklare i varje större agentprojekt.

Den mänskliga insatsen var liten, men inte noll. Tianyi Peng gav enstaka instruktioner på övergripande nivå, till exempel att prioritera Jacobi-varieteten som schema eller att snabbt avsluta Mazurs sats. Enligt den citerade agentutskriften rapporterade systemet rotresultatet som bevisat den 18 augusti klockan 02:00:57 UTC.

Från olympiaden till Erdős-problem: AI-bevis sedan 2024

Fermat-meddelandet står inte ensamt. Sedan 2024 visar flera resultat att AI kan bevisa matematik, och de skiljer sig åt i om Lean användes.

I juli 2024 löste AlphaProof tillsammans med AlphaGeometry 2 fyra av sex uppgifter i den internationella matematikolympiaden och nådde 28 av 42 poäng, silvernivå. Guldgränsen låg på 29 poäng. AlphaProof bevisar i Lean och löste bland annat tävlingens svåraste uppgift. Uppgifterna hade dock dessförinnan översatts för hand till formellt språk, och beräkningstiden var upp till tre dagar per uppgift. Deltagarna har två gånger 4,5 timmar.

I juli 2025 nådde Gemini Deep Think 35 av 42 poäng, guldnivå, officiellt bedömt av olympiadens koordinatorer. Systemet arbetade på naturligt språk inom tidsgränsen och utan Lean. Det är en medveten kontrast: Även utan formell kontroll blir AI stark, men resultaten är då inte maskinellt verifierade utan måste läsas av människor. Företaget Harmonic beskriver i en publikation på arXiv sitt system Aristotle, som kombinerar Lean-baserad bevissökning med informellt resonerande och en geometrilösare och enligt sammanfattningen når guldnivå på uppgifterna från 2025.

I början av 2026 hamnade Erdős-problemen i blickfånget, en stor samling öppna frågor från matematikern Paul Erdős. Ett exempel är problem 728, vars bevis av Aristotle i Lean är dokumenterat i en utarbetning på arXiv. Enligt Simons Foundation löste dessutom en 23-åring i början av 2026 problem 1196 med ChatGPT och Lean.

Bedömningen blir försiktig. Terence Taos wiki om AI-bidrag till Erdős-problem uppfattar sig uttryckligen inte som ett riktmärke. Den nämner en urvalsbias, eftersom framgångar dokumenteras oftare än misslyckanden. Den påpekar att uteblivna tidigare framsteg ofta tyder på obekantskap snarare än svårighet, att redan befintlig litteratur ofta dykt upp i efterhand och att ett löst problem inte automatiskt är ett arbete redo för publicering. Samtidigt rekommenderar wikin att AI-bevis kontrolleras formellt i Lean.

Fältet för AI-bevis i matematiken spänner från tävlingsuppgifter via perifera problem till stora formaliseringar. Utvecklingen går snabbt framåt; om varje meddelande håller vad rubriken lovar måste prövas för sig. Just för det är ett kontrollverktyg som Lean tänkt.

Vad är 11 dagar värda? Tidsjämförelse utan överdrifter

Siffrorna inbjuder till stora jämförelser. Fermat formulerade satsen 1637, Wiles bevisade den 1995, det är 358 år. Formaliseringsprojektet vid Imperial College startades 2024, med en blueprint på 86 sidor, och var ursprungligen planerat för flera år. AI-formaliseringen tog 11 dagar.

Den jämförelsen halkar av flera skäl:

• De 11 dagarna är körtiden för en agentsvärm, inte beräkningstiden för en enskild modell.
• Beviset var känt. AI:n behövde inte hitta någon ny idé, utan översätta en befintlig bevisstruktur till Lean.
• Det fanns förarbete: Mathlib, material från Imperial-projektet och från flt-regular samt en blueprint.
• Insatsen på cirka sex miljarder output-tokens från en intern modell är betydande. Kostnader i pengar anges inte.

Att likställa 11 dagars AI-arbete med århundraden av mänskligt arbete med problemet är därför bara en retorisk jämförelse. Riktigt är: Ett arbete som ett gemensamt projekt hade planerat för flera år blev i allt väsentligt färdigt på några dagar.

Ett sidoexperiment riktar blicken mot vardagen. Enligt Anthropic formaliserade tre personliga Claude-Max-abonnemang Vinogradovs tre-primtalssats på tre dagar. Författarna anser att gemensam formalisering med konsumentabonnemang är möjlig om ramverket stämmer. Det är en bedömning från författarna och inte ett oberoende belagt resultat.

Gränser och öppna punkter: vad meddelandet inte visar

Anthropic nämner själva begränsningar. Beviset är sannolikt märkbart längre än nödvändigt, eftersom Mathlib är kompaktare och bättre granskat. Det beror på vad som redan är formaliserat i Mathlib. Modellen som användes är en intern, icke-offentlig forskningsmodell, så resultatet kan inte upprepas utifrån med samma medel.

Ytterligare punkter förblir öppna:

• Ingen ny matematik skapades. Formaliseringen ökar visshet, inte kunskap.
• Ett bevis i Lean är inte automatiskt begripligt. 13 miljoner rader läser ingen från början till slut.
• Lean säger inget om en sats betydelse, bara om dess korrekthet.
• Hur oberoende kontrollen är utöver Buzzards bedömning framgår inte av meddelandet.

För ytterligare enskilda meddelanden, till exempel om framsteg kring Riemannhypotesen eller om autoformaliseringsagenter från enskilda företag, finns i den här researchen inga primärkällor som går att kontrollera själv. De meddelandena lämnas därför här utan siffror. Enskilda experters bedömningar tas också bara med när originalutsagan finns tillgänglig.

Vad Lean-ansatsen betyder utanför matematiken

Mönstret bakom Fermat-projektet går att generalisera: fritt provande på ena sidan, hård kontroll på den andra. Det passar överallt där ett resultat kan kontrolleras maskinellt. Lean-sidan nämner som tillämpningar utanför matematiken verifieringen av ArkLib, ett bibliotek för SNARK (kompakta kryptografiska bevis), och av Cedar, AWS auktoriseringsspråk. I programvaruutveckling är principen välkänd: En kompilator och en testkörning godkänner likaså det som en människa eller en AI har skrivit.

För hanteringen av AI-utdata ger det en tumregel. Ju bättre ett resultat kan kontrolleras automatiskt, desto tryggare kan en modell arbeta fritt. För texter, bedömningar och rekommendationer saknas oftast den hårda kontrollen. Där förblir människan granskaren.

Samma logik gäller för säkerhet och dataskydd: Bevisbara egenskaper väger tyngre än blotta påståenden. Om en webbplats till exempel laddar spårare eller sätter säkerhetsheaders går att mäta automatiskt. Det erbjuder Dr. DSGVO:s webbplatskontroll, och tekniska säkerhetsegenskaper kan kontrolleras med Security-Checks. Ingen av dem är formella bevis i Leans mening, men de följer samma tanke: mäta i stället för att tro.

Försök av Dr. DSGVO

Med hjälp av AI har (sannolikt) det matematiska beviset tagits fram och formaliserats att magiska hexagoner enligt en viss konstruktionsregel finns för varje godtyckligt n (n = kantlängd för en sexhörning i vaxkakor).

Den totala AI-beräkningstiden var knappt 9 timmar. Av den arbetade systemet i princip 99,9 % av tiden autonomt och behövde inga inmatningar. Bevisfilernas omfång var 173 MB! Formaliseringen med Lean inklusive bibliotek tog knappt 8 GB lagringsutrymme på hårddisken – i mellansteg! Hela beviset sträckte sig över 5 dagar. Det avbröts på grund av användningsgränser eller liknande.

Inom kort publiceras beviset här. Om det är korrekt måste kunniga personer bedöma, som förstår mer av matematik än författaren, som använde AI 😉

Slutsats: Revolutionen är kontrollerbarheten

AI:n har inte bevisat Fermats sista sats på nytt, utan formaliserat Wiles bevis fullständigt i Lean, enligt Anthropic på 11 dagar med flera dussin parallella agenter. Framgången vilar på två saker: en organisation som håller projektets status synlig, och Lean bevisassistent, som bara godtar det som följer.

Utvecklingen sedan 2024 visar att AI allt oftare levererar matematiska bevis. Hur mycket av det som är nytt och hur mycket som är känt material måste bedömas för sig, även Tao-wikin manar till det. Där Lean är med förblir korrektheten kontrollerbar. Det är den verkliga framgången: inte fler påståenden, utan maskinellt kontrollerad visshet.