Lean bevisassistent og AI: Sådan bliver beviser maskinelt kontrollerbare

Elleve dage, en sværm af agenter, 13 millioner linjer kode: En AI har gjort beviset for Fermats sidste sætning maskinelt kontrollerbart. Det afgørende var mindre regnekraften end en kontrollør, der ikke lader nogen fejl slippe igennem.

Omkring 1637 noterede Pierre de Fermat en påstand i marginen af en bog, som han angiveligt havde et bevis for. Det blev aldrig fundet. Først i 1995 offentliggjorde Andrew Wiles et fuldstændigt bevis. Den 4. september 2026 meldte Anthropic så, at en sværm af Claude-agenter har formaliseret dette bevis fuldstændigt i bevissproget Lean. Det blev muligt med Lean bevisassistenten, som kontrollerer hvert trin i et bevis maskinelt.

Indlægget sætter meldingen i perspektiv. Det forklarer, hvad en bevisassistent er, og hvorfor et resultat fra Lean regnes for pålideligt. Det beskriver, hvordan agenterne arbejdede sammen, og stiller meldingen ved siden af olympiadeopgaver og Erdős-problemer. Undervejs holdes dokumenterede tal, producentoplysninger og åbne spørgsmål adskilt. Teserne er: Det nye er ikke kun, at en AI arbejder matematisk. Det nye er kombinationen af en model, der må prøve frit, og et program, der ubestikkeligt godkender hvert trin.

Fermats sidste sætning: Hvad Anthropic faktisk har meldt

Sætningen siger, at ligningen aⁿ + bⁿ = cⁿ ikke har nogen løsning i hele tal større end nul med en eksponent n større end 2. Udsagnet er nemt at forstå og var i århundreder ekstremt svært at bevise. I 1908 blev der udsat en pris på 100.000 guldmark, og ifølge Anthropic indløb der det første år 621 forkerte beviser. Wiles fremlagde et bevis i 1993, fandt et hul og lukkede det sammen med Richard Taylor. Offentliggørelsen fulgte i maj 1995.

Den seneste melding handler om, hvor sikkert dette bevis er, når hvert trin kontrolleres af en maskine. De centrale oplysninger fra Anthropics offentliggørelse står i tabellen.

Et token er her en lille tekstbyggesten, som en sprogmodel producerer, for eksempel en orddel. Kilden oplyser ingen pengeomkostninger. Alle oplysninger stammer fra producenten og er ikke talt efter uafhængigt i denne form.

Afgrænsningen er vigtig. Der er tale om en formalisering, ikke et nyt bevis. Sætningen har været bevist siden 1995. Ifølge Anthropic byggede agenterne på en forenklet udgave af Wiles-beviset fra Darmon, Diamond og Taylor og overtog dele fra formaliseringsprojektet på Imperial College og projektet flt-regular. Den, der læser om en AI-løsning af Fermats sætning, bør derfor ikke tænke på en ny matematisk opdagelse, men på en verifikation. Anthropic afgrænser udtrykkeligt resultatet fra AI-arbejdet med Riemann-hypotesen, hvor der efter sigende er opdaget noget nyt.

Hvad er Lean? En bevisassistent, der ikke springer noget trin over

Lean bevisassistenten er et open source-programmeringssprog, hvor matematiske beviser kan nedskrives, så en computer kan kontrollere dem. Projektsiden lean-lang.org beskriver Lean som programmeringssprog og bevisassistent med en minimal, pålidelig kerne, der sikrer korrektheden. Lean er udviklet af Leonardo de Moura og blev udgivet som open source i 2013, som Simons Foundation beretter. Siden 2023 har den almennyttige Lean FRO arbejdet videre med udviklingen, blandt andet støttet med 5 millioner amerikanske dollar fra Simons Foundation International.

Princippet kan siges i hverdagssprog. Et bevis i Lean er et program. Leans kerne kontrollerer trin for trin, om hver slutning følger af aksiomerne og af allerede kontrollerede sætninger. Aksiomer er matematikkens grundantagelser, som gælder uden bevis. Et trin, der ikke følger, afvises, uanset hvor overbevisende det lyder. Hvor et bevis stadig mangler, står pladsholderen „sorry“ i Lean. Et bevis med sådanne pladsholdere regnes for ufuldstændigt.

Netop det gør Lean så nyttigt for AI-modeller. Sprogmodeller kan formulere overbevisende og samtidig begå fejl. I matematikken er det et problem, for en fejl i trin 400 kan gøre alt efterfølgende værdiløst. Med en bevisassistent som Lean bortfalder spørgsmålet om, hvorvidt modellen kan stoles på.

En menneskelig bedømmelse fungerer anderledes. Fagfolk læser et bevis, finder det plausibelt og stoler på deres erfaring. Det er værdifuldt, men tager tid og levner plads til det oversete. Allerede i 2021 validerede et fællesskabsprojekt i Lean et komplekst bevis af Peter Scholze, som Simons Foundation beskriver. Kontrollen fra bevisassistenten erstatter ikke den matematiske forståelse, men den giver vished om korrektheden.

Forløbet i figur 1 viser arbejdsdelingen: Modellen kommer med forslag, Lean-kernen afgør. Om et forslag stammer fra et menneske, en model eller en tilfældighedsgenerator, har ingen betydning for afgørelsen.

Mathlib og spørgsmålet om, hvem der kontrollerer det kontrollerede

Lean alene indeholder endnu ingen matematik. Den ligger i Mathlib, det fællesskabsudviklede bibliotek, som næsten alle formaliseringer bygger på. Lean-siden nævner mere end en million linjer. Fællesskabets statistikside viste ved opslaget 139.391 definitioner, 290.502 teoremer og 772 bidragydere. Den, der beviser noget i Lean, kan trække på disse kontrollerede byggesten i stedet for at starte fra nul.

Til sammenligning: Fermat-beviset har ifølge Anthropic omkring 13 millioner linjer og er dermed mere end fem gange så stort som Mathlib. Det lyder som en enorm nybygning, men viser også, hvor meget formel verifikation koster ved dybe sætninger, selv når Mathlib leverer fundamentet. Beviset afhænger af det, der allerede er formaliseret i Mathlib.

To kontrolspørgsmål skal stilles hver for sig. For det første: Er beviset korrekt? Det besvarer Lean. Anthropic oplyser, at kun de tre standardaksiomer bruges. For det andet: Blev Fermats sætning virkelig bevist og ikke et ændret udsagn? Her blev der brugt et Comparator-værktøj, som bekræftede, at det formaliserede udsagn stemmer overens med formuleringen i Mathlib. Denne adskillelse er afgørende. Et fejlfrit bevis for et forkert udsagn ville være værdiløst.

Det fulde bevis ligger ifølge Anthropic sammen med en skriftlig forklaring på GitHub og kan ses der. Kun den anvendte model er ikke offentlig.

Kevin Buzzard fra Imperial College London, der har ledet formaliseringsprojektet siden 2024, gennemgik beviset. Ifølge Anthropic fastslår han, at sætningen bevises uden andre forudsætninger end matematikkens aksiomer. En grænse består: Lean kontrollerer korrekthed, ikke betydning. Om et resultat er interessant, elegant eller vigtigt, vurderer værktøjet ikke. Simons Foundation gengiver tilsvarende vurderinger fra Alex Kontorovich.

Agentisk AI: Hvorfor sværmen virkede

Flere dusin agenter arbejdede parallelt. En agent er i denne sammenhæng en sprogmodel, der ikke kun svarer, men selvstændigt bruger værktøjer, redigerer filer og kontrollerer mellemresultater. Multi-agent-rammen byggede på Claude Code. Agenterne definerede begreber, beviste mellemsætninger og brugte dem til sværere udsagn. En generel introduktion giver indlægget AI-agenternes tidsalder.

Gennembruddet kom ifølge Anthropic ikke fra en stærkere model, men fra en bedre organisation. Platformen Prove2Me, en åben samarbejdsplatform fra Tianyi Peng og kolleger ved Columbia University, tilbød tre egenskaber:

• En rettet acyklisk graf over teoremudsagnene gav overblik: Hvert udsagn viser, hvad det afhænger af, og der er ingen kredse.
• Udsagn og beviser lå i separate filer. Det fremskynder Lean-kompileringen, fordi alt ikke skal kontrolleres igen ved hver ændring.
• Allerede beviste sætninger kunne søges frem og genbruges via beskrivelser i naturligt sprog.

Tidligere forsøg uden denne struktur strandede, fordi agenterne mistede overblikket over projektets stand. Det er oplysende, at disse forsøg alligevel bidrog med omkring 7 procent af de ikke-trivielle linjer i det endelige bevis. Læren: Ved store opgaver slår struktur den rå modelstyrke. Den, der sætter mange agenter i arbejde, har brug for en fælles plan, delt lager og klare ansvarsområder. Samme erfaring gør udviklere i ethvert større agentprojekt.

Den menneskelige andel var lille, men ikke nul. Tianyi Peng gav lejlighedsvis anvisninger på overordnet niveau, for eksempel at prioritere Jacobi-varieteten som skema eller at afslutte Mazurs sætning hurtigt. Ifølge det citerede agentoutput meldte systemet rodresultatet bevist den 18. august kl. 02:00:57 UTC.

Fra olympiaden til Erdős-problemer: AI-beviser siden 2024

Fermat-meldingen står ikke alene. Siden 2024 har flere resultater vist, at AI kan bevise matematik, og de adskiller sig ved, om Lean blev brugt.

I juli 2024 løste AlphaProof sammen med AlphaGeometry 2 fire af seks opgaver ved den internationale matematikolympiade og nåede 28 af 42 point, sølvniveau. Guldgrænsen lå på 29 point. AlphaProof beviser i Lean og løste blandt andet konkurrencens sværeste opgave. Opgaverne var dog først oversat i hånden til formelt sprog, og regnetiden var op til tre dage pr. opgave. Deltagerne har to gange 4,5 time.

I juli 2025 nåede Gemini Deep Think 35 af 42 point, guldniveau, officielt bedømt af olympiadens koordinatorer. Systemet arbejdede i naturligt sprog inden for tidsgrænsen og uden Lean. Det er en bevidst kontrast: Også uden formel kontrol bliver AI stærk, men resultaterne er så ikke maskinelt verificeret, men skal læses af mennesker. Virksomheden Harmonic beskriver i en offentliggørelse på arXiv sit system Aristotle, der forener Lean-baseret bevissøgning med uformel ræsonnering og en geometriløser og ifølge abstractet opnår guldniveau på opgaverne fra 2025.

I begyndelsen af 2026 kom Erdős-problemerne i fokus, en stor samling åbne spørgsmål fra matematikeren Paul Erdős. Et eksempel er problem 728, hvis bevis ved Aristotle i Lean er dokumenteret som udarbejdelse på arXiv. Ifølge Simons Foundation løste desuden en 23-årig i begyndelsen af 2026 problem 1196 med ChatGPT og Lean.

Vurderingen fælder forsigtig. Terence Taos wiki om AI-bidrag til Erdős-problemer forstår sig udtrykkeligt ikke som en benchmark. Den nævner en udvælgelsesbias, fordi succeser dokumenteres oftere end fiaskoer. Den peger på, at manglende tidligere fremskridt ofte tyder på ukendthed frem for sværhedsgrad, at allerede eksisterende litteratur ofte dukkede op bagefter, og at et løst problem ikke automatisk er et publiceringsklart arbejde. Samtidig anbefaler wikien at kontrollere AI-beviser formelt i Lean.

Feltet AI-beviser i matematikken spænder fra konkurrenceopgaver over randproblemer til store formaliseringer. Udviklingen går hurtigt; om hver melding holder, hvad overskriften lover, må vurderes hver for sig. Netop til det er et kontrolværktøj som Lean tænkt.

Hvad er 11 dage værd? Tidssammenligning uden overdrivelse

Tallene inviterer til store sammenligninger. Fermat formulerede sætningen i 1637, Wiles beviste den i 1995, det er 358 år. Formaliseringsprojektet på Imperial College startede i 2024 med en blueprint på 86 sider og var oprindeligt tænkt til at vare flere år. AI-formaliseringen varede 11 dage.

Denne sammenstilling halter af flere grunde:

• De 11 dage er kørselstiden for en agentsværm, ikke regnetiden for en enkelt model.
• Beviset var kendt. AI'en skulle ikke finde en ny idé, men oversætte en eksisterende bevisstruktur til Lean.
• Der var forarbejde: Mathlib, materiale fra Imperial-projektet og fra flt-regular samt en blueprint.
• Indsatsen på omkring seks milliarder output-tokens fra en intern model er betydelig. Pengeomkostninger er ikke oplyst.

At sidestille 11 dages AI-arbejde med århundreders menneskeligt arbejde med problemet er derfor kun en retorisk sammenligning. Rigtigt er: Et arbejde, som et fællesskabsprojekt havde planlagt over år, blev i det væsentlige færdiggjort på få dage.

Et sideeksperiment retter blikket mod hverdagen. Ifølge Anthropic formaliserede tre personlige Claude Max-abonnementer Vinogradovs tre-primtals-sætning på tre dage. Forfatterne anser fælles formalisering med forbrugerabonnementer for mulig, når rammen er rigtig. Det er forfatternes vurdering og ikke et uafhængigt dokumenteret resultat.

Grænser og åbne punkter: Hvad meldingen ikke viser

Anthropic nævner selv begrænsninger. Beviset er formentlig betydeligt længere end nødvendigt, for Mathlib er mere kompakt og bedre kontrolleret. Det afhænger af det, der allerede er formaliseret i Mathlib. Den anvendte model er en intern, ikke offentlig forskningsmodel, så resultatet ikke udefra kan gentages med de samme midler.

Yderligere punkter forbliver åbne:

• Der er ikke skabt ny matematik. Formaliseringen øger visheden, ikke viden.
• Et bevis i Lean er ikke automatisk forståeligt. 13 millioner linjer læser ingen fra ende til anden.
• Lean siger intet om en sætnings betydning, kun om dens korrekthed.
• Hvor uafhængig kontrollen er ud over Buzzards vurdering, fremgår ikke af meldingen.

Til yderligere enkeltmeldinger, for eksempel om forbedringer af Riemann-hypotesen eller om autoformaliseringsagenter fra enkelte firmaer, foreligger der i denne research ingen primærkilder, som kan efterprøves. Disse meldinger forbliver derfor her uden tal. Også enkelte fagfolks vurderinger overtages kun, når den oprindelige udtalelse foreligger.

Hvad Lean-tilgangen betyder ud over matematikken

Mønstret bag Fermat-projektet kan generaliseres: frit forsøg på den ene side, hård godkendelse på den anden. Det passer overalt, hvor et resultat kan kontrolleres maskinelt. Lean-siden nævner som anvendelser uden for matematikken verifikationen af ArkLib, et bibliotek om SNARKs (kompakte kryptografiske beviser), og af Cedar, AWS' autorisationssprog. I softwareudvikling er princippet kendt: En compiler og en testkørsel godkender ligeledes, hvad et menneske eller en AI har skrevet.

For omgangen med AI-output giver det en tommelfingerregel. Jo bedre et resultat lader sig kontrollere automatisk, desto sikrere kan en model arbejde frit. Ved tekster, vurderinger og anbefalinger mangler denne hårde godkendelse som regel. Dér forbliver mennesket kontrolløren.

Samme logik gælder for sikkerhed og databeskyttelse: Påviselige egenskaber tæller mere end blotte påstande. Om en hjemmeside for eksempel indlæser trackere eller sætter sikkerhedsheadere, kan måles automatisk. Dertil tilbyder Dr. DSGVOs webstedstjek en mulighed, og tekniske sikkerhedsegenskaber kan kontrolleres med Security-Checks. Begge er ikke formelle beviser i Leans forstand, men følger samme tanke: måle frem for at tro.

Forsøg fra Dr. DSGVO

Ved hjælp af AI blev (sandsynligvis) det matematiske bevis ført og formaliseret for, at magiske hexagoner efter en bestemt konstruktionsregel eksisterer for et vilkårligt n (n = kantlængden af en sekskant målt i vabler).

Den samlede AI-regnetid var knap 9 timer. Heraf arbejdede systemet stort set 99,9 % af tiden autonomt og krævede ingen input. Bevisfilernes omfang var 173 MB! Formaliseringen med Lean inklusive biblioteker brugte knap 8 GB lagerplads på harddisken – i mellemtrin! Hele beviset strakte sig over 5 dage. Det blev afbrudt på grund af brugsgrænser eller lignende.

Snart bliver beviset offentliggjort her. Om det er rigtigt, må dygtige personer vurdere, som forstår mere af matematik end forfatteren, der brugte AI 😉

Konklusion: Revolutionen er kontrollerbarheden

AI'en har ikke bevist Fermats sidste sætning på ny, men formaliseret Wiles' bevis fuldstændigt i Lean, ifølge Anthropic på 11 dage med flere dusin parallelle agenter. Succesen hviler på to ting: en organisation, der holder projektets stand synlig, og Lean bevisassistenten, der kun accepterer det, som følger.

Udviklingen siden 2024 viser, at AI i stigende grad leverer matematiske beviser. Hvor meget af det der er nyt, og hvor meget der er kendt materiale, må vurderes hver for sig, det formaner også Tao-wikien til. Hvor Lean er med, forbliver korrektheden kontrollerbar. Det er den egentlige fremgang: ikke flere påstande, men maskinelt kontrolleret vished.