De formalisering van de Laatste Stelling van Fermat

We delen hier het eerste volledige, door een computer gecontroleerde bewijs van de Laatste Stelling van Fermat. Claude heeft gedurende 11 dagen grotendeels autonoom gewerkt om het bewijs te schrijven in de programmeertaal Lean. Hieronder beschrijven we hoe de formalisering is uitgevoerd en delen we enkele gedachten over wat dit werk zou kunnen betekenen voor wiskundig onderzoek.

Rond 1637 noteerde Pierre de Fermat in de kantlijn van zijn exemplaar van de Arithmetica van Diophantus een bewering die een van de beroemdste wiskundige vermoedens aller tijden zou worden: er zijn geen positieve gehele getallen $a, b, c$ die voldoen aan $a^n + b^n = c^n$ voor elke $n > 2$. De Laatste Stelling van Fermat (FLT), zoals het vermoeden bekend werd, bleek ongelooflijk moeilijk te bewijzen. Het eerste bewijs, geleverd door Sir Andrew Wiles in 1995, telde 129 pagina's en vereiste maanden van nauwgezet werk om te verifiëren.

Een decennium later stelde de Nederlandse informaticus Jan Bergstra voor om het bewijs van Wiles te "formaliseren": het omzetten van de wiskundige redenering in een vorm die computers automatisch kunnen controleren. Sindsdien hebben wiskundigen de methoden ontwikkeld die nodig zijn om een zo complex bewijs te coderen, waaronder een meerjarige gemeenschapsinspanning die in 2024 werd gestart door Kevin Buzzard van het Imperial College London om de formalisering te voltooien met behulp van de bewijsassistent Lean.

Onlangs stelde Tianyi Peng, een onderzoeker bij Anthropic wiens groep aan de Columbia University tools bouwt voor AI-formalisering, voor om te testen of Claude vooruitgang kon boeken bij het formaliseren van FLT. Het resultaat ging verder dan hij had verwacht. In 11 dagen tijd produceerde Claude, terwijl hij grotendeels autonoom werkte, het eerste volledige, door een computer gecontroleerde bewijs van FLT. Tijdens dit proces schreef het model 13 miljoen regels Lean en bewees het 29.500 tussenliggende stellingen.

We hebben het resulterende bewijs gedeeld met Kevin Buzzard, die verklaarde:

"Deze buitengewone prestatie op het gebied van autoformalisering, die volgens Anthropic-onderzoekers slechts 11 dagen duurde, bewijst de Laatste Stelling van Fermat zonder andere aannames dan de axioma's van de wiskunde. Onderweg zien we de autoformalisering van algebra, harmonische analyse, meetkunde en getaltheorie, en we leren dat AI-autoformaliseringsartefacten nu robuust genoeg zijn om op voort te bouwen; het bewijs is gelaagd."

Het automatisch formaliseren van een bewijs dat zo complex is als FLT is een belangrijke stap naar een toekomst waarin alle wiskunde gemakkelijk gecontroleerd kan worden. Naarmate AI steeds meer bewijzen produceert, kan het vermogen om werk eenvoudig te formaliseren de last van het evalueren van nieuwe resultaten (een proces dat jaren kan duren) verlichten. We hopen dat het makkelijker, en niet moeilijker, zal worden om de kennisbasis waarop de wiskunde is gebouwd te vertrouwen.

De uitdaging van het verifiëren van wiskundige bewijzen

In tegenstelling tot recent AI-gestuurd werk aan de Riemann-hypothese, dat nieuwe wiskunde produceerde, is hier de verificatie wat nieuw is — het controleren van een wiskundig bewijs zoals men een wiskundige berekening met een rekenmachine zou controleren. Het bewijzen van wiskundige stellingen vereist het samenstellen van complexe logische ketens, en als één enkele schakel breekt, kan alles wat daarop volgt onjuist blijken te zijn. Het diepgaand begrijpen van een nieuw resultaat om zeker te zijn van de correctheid kan maanden, of zelfs jaren, werk kosten.

De Laatste Stelling van Fermat is hiervan een illustratief voorbeeld. Fermat schreef de stelling in de kantlijn van een boek, samen met een prikkelende opmerking:

"Ik heb een werkelijk wonderbaarlijk bewijs hiervan ontdekt, maar deze kantlijn is te smal om het te bevatten."

Meer dan 350 jaar lang zochten generaties wiskundigen naar een bewijs van FLT, wonderbaarlijk of niet. In 1908 werd een prijs van 100.000 Duitse goudmarken (equivalent aan 1 tot 2 miljoen dollar vandaag) uitgeloofd voor iedereen die een correct bewijs kon leveren; in het eerste jaar alleen al werden 621 onjuiste pogingen ingediend.

In juni 1993 presenteerde Wiles wat hij geloofde dat het eerste correcte bewijs van FLT was, in een reeks lezingen van drie dagen. Twee maanden na een intensieve verificatie door verschillende wiskundigen, stelde een reviewer Wiles een vraag die een kritiek gat blootlegde. Wiles besteedde een jaar aan het proberen dit te herstellen, eerst alleen en daarna met zijn voormalige student Richard Taylor. Hij stond op het punt het project op te geven toen hij besefte dat een benadering die hij eerder had verworpen, het bewijs kon repareren.

Wiles publiceerde het eerste correcte bewijs van FLT in mei 1995; dit leunde op moderne wiskundige technieken die ver buiten gingen wat Fermat in 1637 had kunnen weten. Omdat er na eeuwen van proberen geen elementair bewijs is gevonden, gelooft de wiskundige gemeenschap nu dat Fermats eigen oorspronkelijke "wonderbaarlijke bewijs" onjuist was.

De formalisering van de Laatste Stelling van Fermat

Een manier om de correctheid van een bewijs te controleren is door een computer dit te laten doen. Bewijsassistenten zoals Lean verifiëren de logica van een bewijs algoritmisch, waardoor de correctheid buiten twijfel wordt gesteld. Het moeilijke deel voor mensen is het herschrijven van het bewijs zodat Lean het kan begrijpen. Waar een bewijs geschreven voor menselijke lezers veel overduidelijke stappen overslaat, moet Lean elke stap zien, hoe triviaal deze ook is. Menselijke bewijzen bouwen bovendien voort op eeuwen aan gepubliceerde werken, terwijl een formalisering begint bij het kleine deel van de wiskunde dat al geformaliseerd is.

Voor FLT werd verwacht dat het formaliseringsproces jaren zou duren. Alleen het blauwdruk die de wiskundige gemeenschap heeft gebruikt om de beginfase van het project te beschrijven, beslaat 86 pagina's.

Claude voltooide het bewijs in 11 dagen en produceerde ondertussen computer-verifieerbare bewijzen voor 30.300 stellingen (waarvan er 29.500 in het uiteindelijke bewijs werden gebruikt). Tientallen Claude-agents werkten samen om concepten te definiëren, tussenliggende stellingen te bewijzen en deze stellingen te gebruiken om steeds complexere beweringen te bewijzen. Met 13 miljoen regels Lean-code is het bewijs van Claude meer dan vijf keer zo groot als Mathlib, de belangrijkste gemeenschapsbibliotheek van wiskundige bewijzen waarop deze stelling voortbouwt.

Tijdlijn van de FLT-formalisering

Het bewijs van Claude volgt een vereenvoudigde versie van het bewijs van Wiles, zoals beschreven door Darmon, Diamond en Taylor. De menselijke wiskundige input was beperkt tot incidentele instructies op hoog niveau van Tianyi: "Jacobiaan als een schema klinkt als een hoge prioriteit," "duw [de] Mazur [stelling] om snel klaar te zijn."

Hieronder volgen fragmenten uit de denkprocessen van Claude terwijl het model zich realiseerde wat het had gepresteerd:

"THE FLT root reads Proved on the site. Historic moment (modulo re-check)."

"!!! The FLT ROOT 62eb32c0 reads PROVED. R = T closed and cascaded to the root. This is the campaign's goal: e2e FLT on prove2me."

"🏁🏁🏁The FLT root reads PROVED on prove2me at 02:00:57Z Aug-18 (10:00:57pm ET Aug-17). Historic moment for this campaign."

Een aantal van de eerste pogingen van Claude mislukte: hoewel agents aanvankelijk succes hadden, verloren ze snel het overzicht over de staat van het project en stopten ze met effectief samenwerken. Deze mislukte pogingen droegen ongeveer 7% bij aan de niet-boilerplate regels in het uiteindelijke bewijs.

De inspanning slaagde toen we overstapten op het gebruik van Prove2Me, een open collaboratief platform voor het formaliseren van wiskunde, ontworpen door Tianyi Peng en zijn medewerkers aan de Columbia University. Prove2Me hielp door:

• Het bijhouden van een gerichte acyclische graaf (DAG) van stellingen, die agents gebruikten om te beslissen welke bewijzen ze vervolgens moesten proberen. Dit was bijzonder nuttig om geheugenverslechtering tegen te gaan en meerdere agents parallel te laten werken.
• Het versnellen van de Lean-compilatie en het minimaliseren van het resourceverbruik door stellingen en bewijzen in verschillende bestanden te scheiden, waarbij de links tussen hen onafhankelijk werden onderhouden.
• Het mogelijk maken van zoeken en hergebruik door een natuurlijke-taalbeschrijving van elke stelling bij te houden, wat resulteerde in een eenvoudiger bewijspad.

Met Prove2Me en een op Claude Code gebaseerde multi-agent harness voltooide een team van agents het bewijs in iets minder dan twee weken. Hierbij werd ongeveer zes miljard output-tokens verbruikt van een algemeen intern onderzoeksmodel dat ongeveer vergelijkbaar is met Claude Fable 5.1. Het voltooide bewijs werd gecontroleerd door Lean; het maakt gebruik van slechts drie standaardaxioma's van Lean, en een comparator bevestigde dat de formulering van de stelling overeenkomt met de formulering van FLT in Mathlib.

Het verminderen van de last van formele verificatie

De snelheid waarmee we in staat waren dit bewijs te produceren, demonstreert dat het nu mogelijk is om grote delen van de wiskunde te formaliseren. Dit kan helpen bij het opsporen van fouten in de bestaande verzameling wiskundige bewijzen en de last van het beoordelen van nieuw werk verminderen. Na het beoordelen van het Lean-bewijs van Claude vertelde Kevin Buzzard ons:

"Als de automatische formalisering van FLT nu mogelijk is, hebben we een grote stap gezet richting de automatische formalisering van de moderne wiskundige literatuur. Dergelijke autoformaliserings-technieken zullen leiden tot nieuwe tools, die fouten in het huidige wiskundige corpus zullen uitroeien en de last voor reviewers zullen verlichten. De technieken zullen ons ook in staat stellen om door LLM's gegenereerde wiskunde rigoureus te controleren, wat momenteel doorgaans een extreem kostbaar, mensgestuurd proces is."

Formalisering is ook een belangrijke factor in hoe mensen vertrouwen kunnen krijgen in door AI gegenereerde wiskundige resultaten. Naarmate AI en AI-ondersteunde wiskundigen meer (vermeende) bewijzen produceren dan ooit tevoren, neemt AI-ondersteunde formalisering een deel van de last van menselijke reviewers over. We verwachten dat het gebruikelijk zal worden om een geformaliseerd bewijs te leveren naast elke uiteenzetting die bedoeld is voor een menselijke lezer. Hoewel we niet denken dat een geformaliseerd bewijs een menselijk begrijpelijke uiteenzetting moet vervangen, is het wellicht de enige haalbare manier voor de wiskundige gemeenschap om bij te blijven met AI-gegenereerde bijdragen.

Het schrijven in Lean lijkt Claude ook te helpen bij het bewijzen van nieuwe resultaten. Veel van onze recente door Claude geschreven resultaten zijn parallel aan hun bewijzen geformaliseerd, en Claude lijkt deze partiële bewijzen te gebruiken om onafhankelijk zijn hypothesen te controleren, vergelijkbaar met hoe het numerieke simulaties schrijft om te controleren of het op het juiste spoor zit.

Het formaliseren van FLT was een token-intensief project, maar het is ook het grootste Lean-bewijs dat ooit is geconstrueerd. Anthropic-onderzoekers deden een klein experiment met drie persoonlijke Claude Max-abonnementen om toepassingen van de Hardy-Littlewood Circle Method te formaliseren. Door volledig via Prove2Me samen te werken, voltooide de agents gezamenlijk een formalisering van de stelling van de drie priemgetallen van Vinogradov in slechts drie dagen. We denken dat, met de juiste ondersteuning, collaboratieve formalisering van grote resultaten met consumenten-AI-abonnementen haalbaar is.

Met dit doel voor ogen hebben Anthropic en andere labs onlangs hun ondersteuning voor externe onderzoekers uitgebreid — inclusief wiskundigen die werken aan zuivere wiskunde en formalisering — met gratis en kortingsabonnementen en onderzoekstegoed. We bieden ook specifieke beurzen aan voor grotere wetenschappelijke projecten, die het formaliseren van andere belangrijke stellingen of het verbeteren van Lean of Mathlib kunnen omvatten.

Nu AI snel verandert hoe wiskundig onderzoek eruitziet, worstelen wiskundigen — bij Anthropic en elders — met wat dat betekent voor hun werk. Formalisering is echter een gebied waar we ons onvoorbehouden goed voelen over de rol van AI. Naarmate formalisering een gebruikelijker instrument wordt, hopen we dat het zal helpen het vertrouwen in de gemeenschappelijke basis van wiskundige kennis te behouden.

Erkenningen

Onze formaliseringsinspanning is een klein onderdeel van de lange geschiedenis van de stelling van Fermat en de ontwikkeling van formele wiskunde. Het eerste volledige bewijs van Andrew Wiles samen met Richard Taylor was het hoogtepunt van meer dan driehonderd jaar wiskunde, waarin ideeën werden geïntegreerd van onder anderen Gerhard Frey, Jean-Pierre Serre, Ken Ribet, Barry Mazur, Robert Langlands, Jerrold Tunnell, Yutaka Taniyama, Goro Shimura en André Weil. Het bewijs van Claude volgt de uiteenzetting van Henri Darmon, Fred Diamond en Richard Taylor.

Ons bewijs past delen aan van het FLT-project van het Imperial College London onder leiding van Kevin Buzzard en het flt-regular project. Lean en Mathlib zijn beide gepassioneerde projecten en hebben bijdragen ontvangen van honderden wiskundigen, waarvan velen werkten met de Lean FRO. We danken Kevin Buzzard voor het beoordelen van het bewijs en voor zijn commentaren.

Meer informatie

Het volledige bewijs is beschikbaar op GitHub, samen met een geschreven uitleg van het bewijs.

Aanbevolen literatuur

• The Proof in the Code is een recent boek over de geschiedenis van de Lean-bewijsvinder en de formalisering van wiskunde.
• De BBC-documentaire "Fermat’s Last Theorem" uit 1996 bevat interviews met Wiles en andere wiskundigen die betrokken waren bij het bewijs.
• Voor wie een wiskundige achtergrond heeft, kan een technische geschiedenis van propositions-as-types (de onderliggende discipline van bewijsassistenten zoals Lean, Rocq en Agda) worden gevonden in Propositions as Types door Philip Wadler.
• Chen, S., Marwaha, K., Lu, X., Yuen, H., & Peng, T. (2026). Prove2Me: An open collaborative platform for scaling math formalization. arXiv. https://doi.org/10.48550/arXiv.2608.28433
• Automating Math, Adam Marblestone, in Asterisk Magazine.

***

Voetnoten

1. Tijdens zijn bachelorstudie wilde de onderzoeksbegeleider van Peng resultaten uit de thesis van Peng opnemen in een Nature-artikel. Hij vroeg Peng of hij er zeker van was dat het bewijs correct was. Pengs eerlijke antwoord was: "Ik ben 99% zeker, maar het is moeilijk om 100% zeker te zijn van een bewijs van deze lengte." Peng miste hierdoor de kans om zijn werk in Nature te publiceren.
2. Er zijn talloze andere verhalen over de wiskundige gemeenschap die worstelt met verificatie. Een van de bekendste is het bewijs van Thomas Hales uit 1998 voor het Kepler-vermoeden, dat vier jaar in review was voordat een panel van 12 referees genoegen nam met "99% zeker" (Hales leidde uiteindelijk een project van twintig personen, Flyspeck, dat het bewijs formaliseerde). Het bewijs van Grigori Perelman uit 2002 voor het Poincaré-vermoeden kostte de gemeenschap ongeveer vier jaar en drie uiteenzettingen van elk 300 pagina's om geaccepteerd te worden. Het bewijs van Harald Helfgott uit 2013 voor het zwakke Goldbach-vermoeden is nog steeds in behandeling. Soms worden resultaten die later onjuist blijken te zijn jarenlang geaccepteerd, en bouwen andere wiskundigen hun theorieën op deze foutieve fundamenten.
3. Dit is mede omdat Mathlib beknopt en goed beoordeeld is, terwijl ons bewijs waarschijnlijk veel langer is dan nodig.