Claude formaliseert Fermat in 13 miljoen regels Lean

Anthropic zegt dat Claude in elf dagen een volledig computergecontroleerd bewijs van Fermats laatste stelling heeft geschreven. Het resultaat staat in de bewijstaal Lean, telt ruim 13 miljoen regels en is daarmee de grootste Lean-formalisering die ooit is gemaakt.

Elf dagen en 6 miljard tokens

In het onderzoeksbericht van Anthropic staat dat het om een intern onderzoeksmodel ging, qua niveau ongeveer vergelijkbaar met Claude Fable 5.1. Dat model produceerde zo’n 6 miljard output-tokens en bewees onderweg 30.300 stellingen, waarvan er 29.500 in het uiteindelijke bewijs terechtkwamen. Er zitten ook 1.450 definities in. Mislukte pogingen leverden nog eens zo’n 7 procent van de regels op.

Ter vergelijking: Mathlib, de standaardbibliotheek waar de Lean-gemeenschap al jaren aan bouwt, is ruim vijf keer kleiner dan wat Claude hier in anderhalve week neerzette.

Claude nam niet de klassieke route van Kummer, die alleen reguliere priemgetallen aankan. Het model werkte met de Frey-kromme en modulariteitslifting, de moderne aanpak van Andrew Wiles en Richard Taylor, in de vereenvoudigde versie van Darmon, Diamond en Taylor.

Lean laat geen sprongen toe

Een bewijsassistent als Lean accepteert geen intuitieve stappen. Klopt een redenering formeel niet, dan compileert de code simpelweg niet. De kernel van Lean heeft dit bewijs geaccepteerd zonder axioma’s buiten de drie standaardaxioma’s, wat betekent dat er geen verborgen aannames in verstopt zitten.

Kevin Buzzard van Imperial College London, die al jaren een eigen Lean-project rond Fermat leidt, bekeek het resultaat. “If the automatic formalization of FLT is possible now, then we have taken a big step towards automatic formalization of the modern mathematical literature”, zei hij erover. Eerder schreven we al over de eerste AI-experimenten binnen dat project, toen nog met losse deelstukken.

Wat er niet gebeurd is

Claude heeft Fermats laatste stelling niet opnieuw bewezen. Het model vertaalde het bestaande menselijke bewijs uit 1994 naar een vorm die een computer kan nalopen. Dat werk leunt zwaar op bibliotheken die Buzzards FLT-project en het flt-regular-project al hadden klaargelegd.

Anthropic zelf noemt het bewijs waarschijnlijk veel langer dan nodig. De eerste pogingen strandden omdat het model de draad kwijtraakte tussen duizenden onderling afhankelijke stellingen. Pas met een intern platform genaamd Prove2Me, dat de afhankelijkheidsgraaf bijhoudt en meerdere agents tegelijk laat werken, kwam er beweging in. De volledige code staat publiek op GitHub, zodat iedereen de keten kan inspecteren.

Dat verschil met eerdere claims is relevant. Toen GPT-5.6 Sol Ultra een wiskundevermoeden claimde te bewijzen, bleef de vraag hangen wie dat controleert, en ook bij Astra’s Lean-bewijs bleef peer review achterwege. Bij een formalisering ligt dat anders: de compiler is de reviewer.

“De winst zit hier niet in slimmer rekenen, maar in geduld. Een model dat elf dagen achter elkaar duizenden bewijsstappen afvinkt zonder te verslappen, doet werk waar mensen simpelweg niet voor gebouwd zijn.”

Leon Tindemans, AI-expert en Copilot- & ChatGPT-trainer, geeft onder meer Copilot-training aan Nederlandse organisaties.

Wat betekent dit

Het narekenen van een groot wiskundig bewijs kost normaal jaren aan menselijke aandacht. Wiles’ oorspronkelijke bewijs had een fout die pas na maanden boven water kwam. Als een model dat controlewerk in elf dagen kan doen, verschuift de flessenhals van verificatie naar het bedenken van nieuwe wiskunde.

Voor wie AI vooral als tekstmachine ziet, is dit een nuttige correctie. Hier telt exact een ding: compileert het of niet. Datzelfde patroon zagen we toen Claude een ondergrens rond de Riemann-zetafunctie opschoof. De volgende vraag is of dit ook werkt op stellingen waar nog geen mens een bewijs voor heeft.