Lean-formalisering: wiskundige bewijzen laten controleren door een computer
Stel je voor dat een wiskundige een ingewikkeld bewijs van tientallen pagina's publiceert, en dat niemand ter wereld helemaal zeker weet of elke stap wel klopt. Dat gebeurt vaker dan je zou denken: grote bewijzen zijn soms zo complex dat zelfs andere experts jaren nodig hebben om ze te controleren, en er zijn gevallen bekend waarin fouten pas na publicatie aan het licht kwamen. Lean-formalisering is een manier om dat probleem aan te pakken door een bewijs niet alleen door mensen, maar ook door een computerprogramma te laten narekenen, tot op het meest elementaire logische niveau.
Lean is de naam van dat programma: een zogeheten 'proof assistant' (bewijsassistent), een soort extreem pietluttige rekenmachine voor logica. Waar een gewone rekenmachine controleert of 2+2 werkelijk 4 is, controleert Lean of elke stap in een wiskundig bewijs logisch geldig is, gebaseerd op een klein aantal fundamentele regels. Een bewijs 'formaliseren' in Lean betekent dat je het herschrijft in een taal die de computer letterlijk, stap voor stap, kan verifiëren — zonder aannames, zonder 'dit is triviaal, dat zien we wel', en zonder menselijke welwillendheid.
Wat is het precies?
Lean is in de kern een programmeertaal met een ingebouwd controlesysteem voor logica, gebaseerd op wiskundige grondslagen die 'typetheorie' heten. Zonder in de techniek te duiken: het komt erop neer dat elke wiskundige bewering en elk bewijsstapje een precieze, ondubbelzinnige vorm krijgt die de computer kan checken tegen een handjevol basisregels van de logica.
Een wiskundige die een bewijs wil formaliseren, typt het bewijs stuk voor stuk in Lean's taal. Bij elke stap probeert het programma te bevestigen dat die stap daadwerkelijk volgt uit de vorige. Klopt iets niet, dan geeft Lean een foutmelding — net zoals een compiler een foutmelding geeft bij een typefout in software. Pas als het hele bewijs, van begin tot eind, door deze controle komt, is het 'geformaliseerd': bewezen op een manier die geen enkele twijfel meer overlaat, want de machine heeft elke logische stap onafhankelijk geverifieerd.
Dat is een heel ander soort werk dan het origineel opschrijven van een wiskundig bewijs. Menselijke wiskundigen laten vaak stappen weg die ze 'evident' vinden, of leunen op intuïtie en ervaring. Voor een computer bestaat 'evident' niet: alles moet expliciet worden gemaakt, tot en met de meest basale rekenregels. Daardoor is het formaliseren van een bewijs vaak veel meer werk dan het bedenken ervan — soms wel tien tot honderd keer zoveel tijd.
Om niet telkens vanaf nul te beginnen, bouwt de Lean-gemeenschap aan een gedeelde bibliotheek van al geformaliseerde definities en stellingen, genaamd Mathlib. Wie een nieuw bewijs wil formaliseren, kan voortbouwen op duizenden al geverifieerde onderdelen — van basale rekenkunde tot geavanceerde algebra en topologie — in plaats van elke keer het wiel opnieuw uit te vinden.
Wat wil men ermee bereiken?
Het belangrijkste doel is zekerheid. Moderne wiskunde is zo specialistisch geworden dat sommige bewijzen alleen door een handvol mensen ter wereld volledig te doorgronden zijn. Als die mensen het oneens zijn, of als er simpelweg te weinig experts zijn om alles grondig na te kijken, ontstaat er twijfel die soms jarenlang blijft hangen. Formalisering in Lean maakt die twijfel in principe overbodig: als de computer het bewijs accepteert, is het correct volgens de regels van de logica, punt uit.
Een tweede doel is het opbouwen van een soort permanente, herbruikbare 'wiskundige infrastructuur'. Mathlib fungeert steeds meer als een naslagwerk waarin definities en stellingen niet alleen zijn opgeschreven, maar ook computerverifieerbaar met elkaar samenhangen. Dat maakt het makkelijker om fouten of inconsistenties in de wiskunde als geheel op te sporen.
Een derde, nieuwer motief is de opkomst van kunstmatige intelligentie. Taalmodellen kunnen tegenwoordig plausibel klinkende wiskundige bewijzen genereren, maar 'plausibel klinkend' is niet hetzelfde als correct. Lean biedt een objectieve scheidsrechter: een AI-systeem kan een bewijs voorstellen, en Lean controleert vervolgens onafhankelijk of het klopt. Dat maakt Lean een aantrekkelijk hulpmiddel voor onderzoek naar AI-systemen die zelfstandig wiskunde kunnen bedrijven, omdat 'gokken tot het werkt' door de formele controle wordt afgestraft.
Voorbeelden uit de praktijk
Het bekendste voorbeeld is het Liquid Tensor Experiment. De Duitse wiskundige Peter Scholze, winnaar van de Fields-medaille, publiceerde eind 2020 een uitdaging: hij twijfelde of een van zijn eigen, zeer technische bewijzen in de zogeheten 'condensed mathematics' wel volledig klopte, en vroeg de Lean-gemeenschap om het te formaliseren. Onder leiding van wiskundige Johan Commelin werd het cruciale onderdeel in de loop van 2021 en 2022 geformaliseerd, waarmee Scholze's bewijs werd bevestigd. Het project trok internationale aandacht als bewijs dat formalisering ook voor actueel, ongepubliceerd onderzoek bruikbaar is.
Een ander opvallend project betreft de Polynomial Freiman-Ruzsa-vermoeden (PFR), een resultaat uit de combinatoriek. Nadat Fields-medaillewinnaar Timothy Gowers en collega's eind 2023 een nieuw bewijs publiceerden, organiseerde de Australisch-Amerikaanse wiskundige Terence Tao — zelf ook Fields-medaillewinnaar — een gezamenlijk project om het bewijs binnen enkele weken volledig in Lean te formaliseren, met hulp van tientallen vrijwilligers wereldwijd. Het liet zien hoe snel een grote, verspreide gemeenschap een vers bewijs kan controleren.
Het Xena Project van Kevin Buzzard, hoogleraar aan Imperial College London, formaliseert al sinds ongeveer 2017 stukken van de universitaire wiskunde-opleiding in Lean, mede om studenten te leren precies te redeneren. Buzzard trekt sindsdien ook de kar achter een ambitieus, meerjarig project om de Laatste Stelling van Fermat — het beroemde getaltheoretische resultaat dat pas in de jaren negentig werd bewezen door Andrew Wiles — volledig in Lean te formaliseren. Dat project, gestart in 2024, wordt gezien als een van de zwaarste formaliseringsopgaven ooit vanwege de omvang en diepgang van het onderliggende bewijs.
Ook op het snijvlak met kunstmatige intelligentie zijn er praktijkvoorbeelden: AlphaProof, een systeem van Google DeepMind, gebruikte Lean als formele 'scheidsrechter' bij het oplossen van opgaven van de Internationale Wiskunde Olympiade. Bij de editie van 2024 haalde het systeem, gecombineerd met een tweede model voor meetkunde, een puntentotaal dat overeenkwam met een zilveren medaille — de bewijzen werden pas als correct erkend nadat Lean ze had geverifieerd.
Hoe ver is de techniek?
Lean-formalisering is volwassen genoeg om grote, serieuze wiskundige resultaten aan te pakken, maar het blijft mensenwerk dat traag en arbeidsintensief is. Mathlib groeit gestaag en telt inmiddels vele honderdduizenden regels geverifieerde wiskunde, met bijdragen van honderden vrijwilligers en professionele wiskundigen wereldwijd, maar het dekt nog altijd maar een fractie van de totale wiskunde die er bestaat.
De grootste bottleneck is de verhouding tussen tijd en resultaat: het formaliseren van een bewijs kost doorgaans veel meer tijd dan het bedenken ervan, omdat elke 'voor de hand liggende' stap alsnog expliciet moet worden gemaakt. Het Fermat-project van Buzzard wordt daarom ingeschat op meerdere jaren werk met een groot team, ook al is het onderliggende wiskundige bewijs al decennia oud en algemeen aanvaard.
Er is de laatste jaren wel duidelijk versnelling merkbaar, vooral doordat AI-systemen worden ingezet om (delen van) formele bewijzen te helpen genereren of automatisch simpele stappen af te handelen — Lean's strikte controle maakt het namelijk mogelijk om AI-voorstellen objectief te beoordelen zonder een mens erbij nodig te hebben voor elke controle. Toch is het nog geen automatisch proces: mensen moeten het overgrote deel van de strategie en creativiteit blijven leveren, en volledig zelfstandige AI-formalisering van geavanceerde, nieuwe wiskunde is nog geen realiteit. Onzeker is ook hoe snel de bredere wiskundige gemeenschap formalisering als standaardpraktijk zal omarmen; op dit moment is het nog vooral een niche binnen de wiskunde, gedreven door een relatief kleine groep enthousiastelingen.
Wie werken eraan?
Lean zelf werd oorspronkelijk ontwikkeld door de Braziliaanse informaticus Leonard(o) de Moura, destijds werkzaam bij Microsoft Research, met de eerste versies daterend van rond 2013. Sindsdien is de ontwikkeling van de programmeertaal zelf ondergebracht bij de Lean Focused Research Organization (Lean FRO), een non-profitorganisatie die specifiek is opgericht om de kerntechnologie te onderhouden en te verbeteren, los van de wiskundige toepassingen.
De formalisering van wiskunde Ãn Lean wordt vooral gedragen door een internationale, grotendeels vrijwillige gemeenschap rond het Mathlib-project, met actieve bijdragen van universiteiten in onder meer het Verenigd Koninkrijk (Imperial College London, met Kevin Buzzard als boegbeeld), de Verenigde Staten en Australië (met Terence Tao als prominente pleitbezorger) en Duitsland (met Peter Scholze en de Universiteit Bonn rond het Liquid Tensor Experiment). Ook grote technologiebedrijven die aan AI voor wiskunde werken, waaronder Google DeepMind en OpenAI, gebruiken Lean als formeel verificatie-instrument voor hun onderzoek naar geautomatiseerd bewijzen. Daarnaast dragen individuele onderzoekers en studenten van over de hele wereld bij aan Mathlib, via een open ontwikkelproces vergelijkbaar met dat van opensourcesoftware.