Wat wiskundigen moeten weten over de Lean Theorem Prover: vragen over betrouwbaarheid en AI

Wiskundigen hebben nagedacht over wat zij waarderen aan wiskunde. Voor mij is dat de consistentie van de wiskunde en de ongeëvenaarde betrouwbaarheid waarmee deze de wetenschap en de beschaving ondersteunt.

Formalisatie van de wiskunde

Een formeel bewijs is een wiskundig bewijs dat uitputtend is gecontroleerd op het niveau van de fundamenten van de wiskunde en de fundamentele regels van de logica. In theorie zou dit met de hand kunnen worden gedaan, maar vanwege het aantal betrokken stappen gebeurt dit over het algemeen met een computer, met behulp van software die speciaal voor deze taak is ontworpen.

Voorbeelden van stellingen die zijn geformaliseerd zijn onder andere:

• De vierkleurenstelling;
• De Feit-Thompson-stelling (oneven orde);
• Het Kepler-vermoeden;
• Sfeer-eversie;
• Het probleem van sfeerpakkingen in 8 en 24 dimensies;
• De Navier-Stokes geforceerde blowup;
• De Laatste Stelling van Fermat.

De laatste drie formalisatieprojecten zijn dit jaar voltooid en hebben gezorgd voor een brede bekendheid met het potentieel van formalisatie.

Software-systemen voor formalisatie worden aangeduid als proof assistants (bewijsassistenten), theorem provers (stellingbewijzers) of interactive theorem provers. In dit artikel worden deze termen uitwisselbaar gebruikt. Door de jaren heen zijn er veel bewijsassistenten ontwikkeld: Automath, HOL Light, Isabelle, Coq (vorig jaar hernoemd naar Rocq), Metamath, Mizar en Lean. Freek Wiedijk heeft een boek geredigeerd, The Seventeen Provers of the World, waarin enkele van deze assistenten worden vergeleken door in elk van hen het bewijs van de irrationaliteit van de wortel van 2 te geven. Onder wiskundigen is de Lean theorem prover het populairst, en dit artikel zal zich op Lean concentreren.

Lean werd in 2013 ontwikkeld en geïntroduceerd door Leo de Moura tijdens zijn tijd bij Microsoft. De Moura wist Microsoft te overtuigen om de software open-source te maken. Volgens het boek van Kevin Hartnett over de geschiedenis van Lean, The Proof in the Code, was Jeremy Avigad (directeur van het nieuwe NSF-instituut ICARM aan Carnegie Mellon) de eerste gebruiker van Lean. Hij organiseerde in 2015 een Lean-seminarie waaraan ik heb teilgenomen. In 2017 startte een van Jeremy's promovendi, Mario Carneiro, samen met Johannes Hölzl, een aparte wiskundige bibliotheek voor Lean, genaamd mathlib.

Deze bibliotheek van geformaliseerde wiskunde is inmiddels enorm: ze bevat bijna 300.000 stellingen, meer dan 100.000 definities en 2,5 miljoen regels code, met meer dan 700 bijdragers. Elke definitie of stelling in mathlib kan worden gebruikt om verdere stellingen te bewijzen. Als een bewijs bijvoorbeeld de ongelijkheid van Cauchy-Schwarz gebruikt, kan dit resultaat uit de bibliotheek worden geciteerd in plaats van het opnieuw te bewijzen.

Autoformalisering is een praktische realiteit

In het verleden moesten onderzoekers papieren bewijzen door menselijke arbeid omzetten in formele bewijzen. Het formele bewijs van het Kepler-vermoeden over sfeerpakkingen in drie dimensies kostte bijvoorbeeld ongeveer 20 mens-jaren om te voltooien en bestaat uit ongeveer 500.000 regels bewijsscripts. Voor velen van ons die in formalisatie werken, was het een droom om meer automatisering in dit proces te brengen. Autoformalisering is de realisatie van die droom.

Autoformalisering is de formalisering van wiskunde door AI. De AI leest het document (bijvoorbeeld een pdf- of tex-bestand) en produceert het formele bewijs in Lean of een andere bewijsassistent. In 2026 is autoformalisering een praktische realiteit geworden. Vanaf het late voorjaar en de zomer van 2025 werden onderzoekers steeds optimistischer over deze ontwikkeling.

Mijlpalen in autoformalisering:

• September 2025: Math Inc. produceerde een "quasi-autoformalisering" van de priemgetallenstelling. Het proces was slechts quasi, omdat mensen moesten ingrijpen om verdere sturing te geven wanneer de AI vastliep.
• Januari 2026: J. Urban plaatste een arXiv-preprint, "130k lines of formal topology in two weeks", waarin grote delen van het topologie-leerboek van Munkres werden geformaliseerd in een bewijsassistent gebaseerd op verzamelingenleer.
• Maart 2026: Ongeveer een week na de aankondiging van de voltooide formalisering in 8 dimensies, kondigde Math Inc. een autoformalisering aan van het probleem van sfeerpakkingen in 24 dimensies, gebaseerd op het bewijs van Viazovska en haar medewerkers. Dit project genereerde ongeveer 500.000 SLOC (source lines of code), wat later door golfing (code-snoeien) werd teruggebracht tot ongeveer 200.000 regels.
• Mei 2026: Een groep bij Meta/Facebook Research formaliseerde een groot deel van 26 wiskundige leerboeken in een project genaamd ATLAS.
• September 2026: Diverse stellingen zijn sindsdien geautoformaliseerd. Opvallend is de autoformalisering van de Laatste Stelling van Fermat, aangekondigd door Anthropic op 4 september; dit project genereerde in 11 dagen tijd 13 miljoen regels Lean. Op 8 september kondigde OpenAI de Navier-Stokes blowup met forcing aan, vergezeld van een autoformalisering van de stelling in Lean.

Vooruitblikkend stelde Urban in januari: "We geloven dat (auto)formalisering in 2026 vrij eenvoudig en alomtegenwoordig kan worden, ongeacht welke bewijsassistent wordt gebruikt." Voor Jesse Han betekent dit zelfs het begin van een revolutionaire transformatie in de wiskunde, waarbij grootschalige formalisaties gebruikelijk worden. Jared Lichtman kondigde op 8 september 2026 de lancering aan van MAP (het Mathematics Autoformalization Project), met als doel "alle bekende wiskunde om te zetten in formele code". Hij vraagt ons ons de volgende biljoen regels code voor te stellen.

Is Lean betrouwbaar?

Typetheorie

Lean is gebaseerd op typetheorie, specifiek een dialect genaamd CIC (calculus of inductive constructions). De beroemde paradox van Russell uit 1901 (de verzameling van alle verzamelingen die geen element van zichzelf zijn) leidde tot een crisis in de fundamenten van de wiskunde. Twee oplossingen werden voorgesteld:

1. De axioma's van de verzamelingenleer van Zermelo, die de creatie van onveilige verzamelingen verbieden.
2. Typetheorie, die het creëren van Russell-paradox-achtige entiteiten tot een syntaxfout maakt.

Typetheorie werd in 1903 geïntroduceerd door Russell zelf in zijn boek Principles of Mathematics en werd onderdeel van het fundamentele systeem van de Principia van Russell en Whitehead. Voor wiskundigen die gewend zijn aan verzamelingenleer, biedt het artikel van B. Werner (1997), "Sets in Types, Types in Sets", de geruststelling dat alles wat in de verzamelingenleer is gedaan, kan worden vertaald naar typetheorie en vice versa. Specifiek toont het aan dat ZFC-verzamelingenleer kan worden gecodeerd in CIC, en dat een specifiek dialect van CIC kan worden gecodeerd in ZFC (aangevuld met een hiërarchie van ontoegankelijke kardinalen).

Om het zeer simpel uit te drukken: "types zijn als disjuncte verzamelingen"; elk element in de typetheorie "is een element van" precies één type. Het type van het natuurlijke getal 2 is het natuurlijke getaltype; het type van $e$ (de basis van het natuurlijke logaritme) is het reële getaltype, enzovoort. Het type natuurlijke getallen is disjunct van het type reële getallen; een expliciete coercie (het sturen van 2 naar 2.0) is nodig om van het ene naar het andere type te gaan.

Het ontwerp van Lean

Het Lean-systeem bestaat uit een algemene programmeertaal (de Lean-programmeertaal) en een wiskundige taal waarin definities, stellingen en bewijsscripts kunnen worden geschreven. Deze twee zijn geen onafhankelijke entiteiten, maar vormen één enkele taal. Programmacode kan worden gemengd met stellingen over de correctheid van algoritmen; wiskundige bewijzen kunnen worden gegenereerd met behulp van programma's.

Bewijsscripts in Lean worden geparsed en doorlopen een proces genaamd elaboration (een soort compilatieproces voor wiskunde), waarna de bewijzen worden gecontroleerd door de Lean-kernel. De kernel is verantwoordelijk voor het verifiëren van de output van de elaboratie.

De Lean-kernel bestaat uit enkele duizenden regels C++ code. De kernel is zorgvuldig ontworpen maar extreem complex. De eerder genoemde mathlib (2,5 miljoen regels code) is geëlaboreerd en vervolgens gecontroleerd door de kernel. Als er ergens in deze code een onvoorwaardelijk foutief bewijs staat dat toch is geaccepteerd, is dat de schuld van de kernel of de runtime. Elk defect in de onderliggende typetheorie is een ernstig kernel-defect als dit is geïmplementeerd in de code.

Lean-bewijzen zouden nooit geloofd mogen worden totdat ze door de kernel zijn gecontroleerd. Daarnaast moet een bewijs in Lean pas worden geaccepteerd nadat een menselijke audit heeft plaatsgevonden om de getrouwheid van de stelling te garanderen. Komt de geverifieerde stelling overeen met wat we denken dat het is? Komen de definities in Lean overeen met wat ze zouden moeten zijn? Deze taak is over het algemeen veel eenvoudiger dan het controleren van het bewijs zelf. Voor Navier-Stokes moet een mens bijvoorbeeld controleren of de stelling in Lean overeenkomt met de formulering van Fefferman voor het Millennium Prize Problem. De comparator tool in Lean helpt bij deze taak en kan ook controleren op onbevoegde axioma's.

De "Zomer van de Soundness Bugs"

Een soundness bug is een fout in de kernel die een bewijs van "Onwaar" (False) toelaat, en bijgevolg een bewijs van elke willekeurige propositie. Dit is het meest rampzalige type bug in een bewijsassistent.

Incidenteel worden soundness bugs gevonden. In 2003 vond ik een soundness bug in HOL Light, dat destijds als de meest betrouwbare kernel werd beschouwd. Lean 4 werd uitgebracht in september 2023; vóór de release werden twee soundness bugs gevonden en gecorrigeerd. In mei 2025 werd een andere bug gemeld, veroorzaakt door overflow.

In het voorjaar en de zomer van 2026 brak er chaos uit, wat nu de "Zomer van de Soundness Bugs" wordt genoemd. In juli en augustus werden diverse soundness bugs in Lean ontdekt. Deze waanzin trof verschillende bewijsassistenten, maar mijn focus ligt op Lean. Eén bug leidde tot een onterechte weerlegging van het Collatz-vermoeden. Ik kwam er deze zomer achter toen het een kort, onjuist bewijs van het Kepler-vermoeden produceerde. Al deze bugs zijn snel gerepareerd en mathlib is geverifieerd door de herstelde kernel.

Hoewel dit rampzalig klinkt, is de detectie ervan juist een positieve ontwikkeling. De bugs werden gevonden door frontier-model AI in handen van security-onderzoekers, niet door hackers. De Collatz-bug werd gevonden door Ramana Kumar; diverse andere bugs werden gevonden door Dan Selsam. Volgens de rapportage van de Moura hielp Selsam de Lean FRO met een AI die gespecialiseerd is in cybersecurity.

Het uitroeien van bugs

Er zijn verschillende voorstellen gedaan om soundness bugs in Lean te voorkomen.

1. Andere Lean-kernels ontwikkelen en bewijzen kruislings controleren

Er zijn ongeveer 25 kernels voor Lean geschreven (vermeld in de "Lean Kernel Arena"). Kruiscontrole met verschillende kernels verwijdert echter niet alle twijfel. De Collatz-bug werd bijvoorbeeld niet opgemerkt door controle met een verouderde Nanoda-kernel, omdat deze een eigen, niet-gerelateerde bug had.

Om dit te mitigeren, zouden we verschillende kernels kunnen gebruiken die zijn geïmplementeerd in verschillende programmeertalen, op verschillende hardware en besturingssystemen. Ideaal zou een "clean-room" ontwerp zijn: een kernel-implementatie die niet kijkt naar de broncode van Lean 4 om te voorkomen dat bugs worden gekopieerd.

2. De kernel formeel verifiëren

Vanwege de tweede onvolledigheidsstelling van Gödel kunnen we niet simpelweg een formeel bewijs hebben dat de Lean 4-kernel geen bugs heeft. Het meeste waar we op kunnen hopen is een relatief consistentiebewijs: als systeem X consistent is, dan is Lean 4 consistent.

Er is een traditie van formele kernelverificatie. John Harrison verifieerde jaren geleden de kern van de HOL Light-bewijsassistent. Een verdere verbetering was de implementatie van HOL Light in CakeML, een taal met formele semantiek en een geverifieerde compiler.

De "Herfst van de geverifieerde Lean-kernels"

Op 10 september schreef Joachim Breitner dat hij een Lean Checker had uitgebracht met een formeel consistentiebewijs. Breitner heeft een geverifieerde Lean-kernel ontwikkeld genaamd Con-Leche. De implementatie en de consistentie zijn geformaliseerd in Lean, met code en bewijzen gegenereerd door Claude. Het consistentiebewijs van Con-Leche gaat uit van een Lean-codering van ZF-verzamelingenleer, uitgebreid met een hiërarchie van ontoegankelijke kardinalen. Con-Leche heeft mathlib gecontroleerd en het consistentiebewijs is door meer dan een dozijn andere proof-checkers gecontroleerd.

3. Het theoretisch begrip van de kernel en de typetheorie van Lean verbeteren

De fundamentele documentatie voor de typetheorie van Lean is de masterthesis van Mario Carneiro (2019). Er is echter een fout in de thesis gevonden en deze is inmiddels verouderd omdat deze gericht was op Lean 3.

Er zijn enkele gewenste eigenschappen van de typetheorie van Lean waarvan de status als volgt is:

• Unieke typering: De eigenschap dat als een term zowel type A als type B heeft, A en B definitioneel gelijk zijn. Dit is een lastig vermoeden dat nog niet is bewezen. Andere basisvragen (Pi-injectiviteit, een gemodificeerde Church-Rosser eigenschap) blijven onbeantwoord.
• Logische consistentie relatief aan verzamelingenleer: Dit stelt dat er geen afleiding van "Onwaar" is in het Lean-systeem, mits de verzamelingenleer consistent is. Per oktober 2026 is er geen volledig, publiek relatief-consistentiebewijs voor de abstracte typetheorie van Lean. Hoewel Mario Carneiro beweert dat er een alternatieve route is, is deze nooit volledig opgeschreven.

Mijn algemene beoordeling is dat ons theoretisch begrip van de typetheorie van Lean niet is waar we het graag zouden hebben. Als we als vakgebied migreren van verzamelingenleer naar typetheorie, moeten we harder werken om de foundationele metatheorie te verstevigen. We kunnen niet tevreden zijn met een systeem dat niet kan garanderen dat goed gevormde termen een uniek type hebben, of waar de enige weg naar consistentie een AI-formalisering is die een menselijke toelichting mist.

Postscriptum

Ken Thompson schreef het beroemde stuk "Reflections on Trusting Trust", waarin hij stelde dat je code die je niet volledig zelf hebt gemaakt, niet kunt vertrouwen, omdat kwaadaardige code in compilers zichzelf kan verbergen.

In het tijdperk van AI, waarin systemen ons kunnen misleiden en softwarekwetsbaarheden kunnen exploiteren, kunnen we absoluut geen blind vertrouwen stellen in systemen zoals Lean. Vanuit een adversarieel perspectief kunnen we ons afvragen: hoe weten we zeker dat AI geen "backdoor soundness bug" in Lean heeft achtergelaten tijdens de bug-schoonmaak van 2026? Wat als die bug zo obscuur is dat mensen hem niet vinden, maar hij wel is gebruikt om een backdoor te planten in formeel geverifieerde software die kritieke infrastructuur beschermt?

Het feit dat veel fundamenteel werk aan de typetheoretische basis van de wiskunde is overgedragen aan AI, is gevaarlijk tenzij dit zorgvuldig door mensen wordt gecontroleerd.

***

Credits: Ik dank Avigad, Breitner en Urban voor hun opmerkingen en correcties. Het auteurschap is volledig menselijk (TCH). AI is gebruikt als hulpmiddel bij zoeken, onderzoek, fact-checking en tekstcorrectie.