Claude formaliseert de laatste stelling van Fermat in Lean

Anthropic maakte op 4 september 2026 bekend dat zijn AI Claude het eerste volledig door een computer geverifieerde bewijs van de laatste stelling van Fermat heeft geleverd, van begin tot eind. De stelling zegt dat er geen positieve gehele getallen a, b, c bestaan die voldoen aan a^n + b^n = c^n voor een geheel getal n groter dan 2. Meer dan dertig jaar nadat wiskundige Andrew Wiles in 1995 zijn 129 pagina's tellende bewijs publiceerde, was de logica ervan nog nooit volledig mechanisch geverifieerd. Claude werkte 11 dagen lang grotendeels autonoom en produceerde daarbij ongeveer 13 miljoen regels code in Lean, een computergestuurde bewijsassistent.

Het project werd geleid door Tianyi Peng, een Anthropic-onderzoeker die zich bezighoudt met AI-gedreven wiskundige formalisering. Onderweg bewees Claude ongeveer 30.300 tussenliggende stellingen in een door de computer verifieerbare vorm, waarvan er ongeveer 29.500 daadwerkelijk in het uiteindelijke bewijs werden gebruikt. De geproduceerde code is meer dan vijf keer zo omvangrijk als Mathlib, de belangrijkste community-wiskundebibliotheek voor Lean. Tientallen Claude-agenten werkten parallel: ze definieerden concepten en bewezen tussenstellingen voordat ze aan steeds lastigere beweringen begonnen. Vroege pogingen mislukten herhaaldelijk: agenten verloren het overzicht over de algehele status van het project en konden elkaars resultaten niet meer effectief hergebruiken. Ongeveer 7% van de niet-repetitieve regels in het uiteindelijke bewijs is afkomstig van die mislukte pogingen.

Wat een door de computer geverifieerd formeel bewijs precies is

Een wiskundig artikel voor menselijke lezers slaat vaak stappen over die als "vanzelfsprekend" gelden. Een bewijsassistent als Lean kan dat niet: elke stap, hoe triviaal ook, moet volledig worden uitgeschreven. Een bestaand bewijs herschrijven naar die vorm heet "formalisering". Omdat één gebroken logische schakel alles wat daarna volgt ongeldig kan maken, krijgt een geformaliseerd bewijs pas een correctheidsgarantie die onafhankelijk is van menselijke controle zodra het de mechanische toets van Lean doorstaat. Het bewijs van Claude steunt uitsluitend op de drie standaardaxioma's van Lean, zonder ook maar één gebruik van "sorry" — de placeholder waarmee een stap tijdelijk onbewezen kan blijven. Een vergelijkingstool bevestigde dat de bewezen bewering exact overeenkomt met de formulering van de laatste stelling van Fermat in Mathlib, en een onafhankelijke, in Rust geschreven Lean-kernel genaamd "nanoda" controleerde meer dan een miljoen declaraties foutloos.

Waarom de laatste stelling van Fermat zo'n symbolisch geval is

De stelling dankt haar naam aan een aantekening die de Franse wiskundige Pierre de Fermat rond 1637 in de kantlijn van een exemplaar van Diophantus' Arithmetica krabbelde: hij beweerde "een werkelijk wonderbaarlijk bewijs" te hebben gevonden, waarvoor de kantlijn te smal was. Meer dan 350 jaar lang zochten generaties wiskundigen tevergeefs naar dat bewijs. In 1908 werd een prijs uitgeloofd die vandaag de dag neerkomt op één tot twee miljoen dollar; alleen al in het eerste jaar kwamen er 621 foutieve bewijzen binnen. In juni 1993 kondigde Andrew Wiles zijn bewijs aan in een reeks lezingen van drie dagen, maar ongeveer twee maanden later, tijdens de verificatie, ontdekte een beoordelaar een kritiek gat. Wiles had, samen met zijn voormalige promovendus Richard Taylor, bijna een jaar nodig om het te herstellen voordat hij in mei 1995 de definitieve versie publiceerde — 129 pagina's, waarvan de verificatie de wiskundige gemeenschap maanden kostte. Opmerkelijk voor een internationale lezer: het vermoeden van Taniyama-Shimura, waarop het bewijs van Wiles steunt, werd in de jaren vijftig geformuleerd door de Japanse wiskundigen Yutaka Taniyama en Goro Shimura. Wat Claude heeft geformaliseerd, is een vereenvoudigde versie van het bewijs van Wiles, afkomstig van Darmon, Diamond en Taylor.

Deze buitengewone autoformaliseringsprestatie, die volgens de onderzoekers van Anthropic slechts 11 dagen kostte, bewijst de laatste stelling van Fermat zonder enige aanname buiten de axioma's van de wiskunde. Onderweg zien we de autoformalisering van algebra, harmonische analyse, meetkunde en getaltheorie, en leren we dat door AI geproduceerde autoformaliseringsartefacten inmiddels robuust genoeg zijn om erop voort te bouwen: het bewijs is meerlagig opgebouwd.

• Werkduur: 11 dagen, grotendeels autonoom
• Geproduceerde Lean-code: ongeveer 13 miljoen regels, meer dan 5 keer Mathlib
• Bewezen stellingen: ongeveer 30.300, waarvan 29.500 gebruikt in het uiteindelijke bewijs
• Verbruikte outputtokens: ongeveer 6 miljard, met een onderzoeksmodel vergelijkbaar met Claude Fable 5.1
• Gebruikte axioma's: alleen de 3 standaardaxioma's van Lean, nul keer "sorry"

Wat Claude werkelijk heeft gedaan — en wat niet

Belangrijk om te benadrukken: Claude heeft het originele bewijs van Wiles niet zelfstandig "ontdekt". De wiskundige redenering zelf werd in 1995 vastgesteld door Wiles en zijn medewerkers; het werk van Claude bestond eruit een vereenvoudigde versie van die redenering te herschrijven naar de strikte symbolische vorm die Lean kan controleren, en die vervolgens mechanisch te laten verifiëren — dat is formalisering, geen ontdekking. Dat is wezenlijk anders dan recent AI-onderzoek naar het vermoeden van Riemann, dat gericht was op het produceren van werkelijk nieuwe wiskunde. Anthropic maakt expliciet duidelijk dat de vernieuwing hier in de verificatie zit, niet in de ontdekking. Het werk leunde op Prove2Me, een samenwerkingsplatform voor wiskundige formalisering ontwikkeld door Tianyi Peng, dat afhankelijkheden tussen stellingen beheert via een gerichte acyclische graaf, zodat meerdere Claude-agenten weten welke stelling ze vervolgens moeten aanpakken. Menselijke inbreng bleef beperkt tot instructies op hoog niveau van Peng, zoals "geef de Jacobiaan als schema prioriteit".

Naarmate AI meer wiskundige bewijzen produceert, groeit de last om die handmatig te controleren. Anthropic verwacht dat het gebruikelijk zal worden om naast een artikel voor menselijke lezers ook een geformaliseerd, door de computer controleerbaar bewijs te leveren. Kevin Buzzard, die sinds 2024 aan het Imperial College London een meerjarig gemeenschapsproject leidt om de laatste stelling van Fermat in Lean te formaliseren — waarvan alleen al het beginplan 86 pagina's beslaat — noemde deze prestatie een grote stap richting de autoformalisering van de moderne wiskundige literatuur: het spoort fouten op in het bestaande corpus, verlicht de last van beoordelaars en maakt het mogelijk door AI gegenereerde wiskunde streng te controleren.

Voor een Nederlands technologie- of onderzoeksbedrijf reikt de les verder dan één wiskundige prestatie. Dezelfde bewijsassistenten die deze stelling hebben geverifieerd, worden al gebruikt om cryptografische protocollen, compilers en veiligheidskritische code in de luchtvaart en chipontwerp te verifiëren — gebieden waarin Nederlandse instellingen als het CWI en verschillende technische universiteiten al lang aan formele methoden werken. Dat een AI-agent binnen dagen in plaats van jaren miljoenen regels machinaal geverifieerd bewijs kan produceren, is een concreet signaal dat formele verificatie, lange tijd beschouwd als te traag en te gespecialiseerd om op te schalen, veel toegankelijker kan worden voor engineeringteams buiten de zuivere wiskunde — mits, zoals Anthropic zelf benadrukt, dit verificatievermogen nooit wordt verward met het vermogen om zelfstandig nieuwe wiskunde te ontdekken.