In 2024 was de Internationale Wiskundeolympiade getuige van een historische mijlpaal. Hoewel de competitie traditioneel een strijd tussen de slimste studenten ter wereld is, stal een onofficiële deelnemer de schijnwerpers: Google DeepMind’s AlphaProof. Het AI-programma behaalde een score op het niveau van een zilveren medaille, wat bewijst dat machines niet langer alleen maar getallen berekenen: ze beginnen de kunst van het logisch redeneren onder de knie te krijgen.
Deze doorbraak is geen geïsoleerd technisch wonder; het is het resultaat van een decennialange evolutie in de manier waarop we de waarheid verifiëren door middel van code. In zijn nieuwe boek, The Proof in the Code, onderzoekt journalist Kevin Hartnett de onwaarschijnlijke reis van Lean, een softwaretool die is getransformeerd van een niche-codeerassistent tot de ruggengraat van moderne wiskundige verificatie en AI-ontwikkeling.
De brug tussen code en logica
Het verhaal begint met Leo de Moura, een voormalige Microsoft Research-ingenieur die Lean in 2013 lanceerde. Oorspronkelijk ontworpen als een hulpmiddel om softwarecode op fouten te controleren, lag het ware potentieel van Lean in de structurele gelijkenis met wiskunde.
Zoals Hartnett opmerkt, delen de twee disciplines een fundamenteel DNA:
– Syntaxis: Beide vereisen nauwkeurige, stapsgewijze instructies.
– Logica: Een enkele fout in een coderegel is functioneel identiek aan een “gat” in een wiskundig bewijs.
– Uitvoering: Net zoals een programma alleen draait als de logica klopt, is een wiskundige stelling alleen geldig als het bewijs ervan waterdicht is.
Dit besef bracht een beweging teweeg. Hoewel Lean op zichzelf geen nieuwe wiskunde kon ‘uitvinden’, fungeerde het wel als een interactieve stellingbewijzer. Er kan een door mensen geschreven bewijs nodig zijn – dat honderden pagina’s kan beslaan en maanden kan duren om door collega’s te worden beoordeeld – en de absolute juistheid ervan in een oogwenk kan worden geverifieerd.
De strijd voor een ‘wiskundige taal’
De overgang van traditionele wiskunde naar digitaal bewijs verliep niet naadloos. Jarenlang werden wiskundigen geconfronteerd met een angstaanjagend ‘kip-en-ei’-probleem: om Lean bruikbaar te maken, hadden ze enorme bibliotheken met gecodeerde wiskundige definities nodig; maar om die bibliotheken te bouwen hadden ze wiskundigen nodig die het programma konden gebruiken.
De wrijving was vaak absurd korrelig. Hartnett beschrijft hoe professor Kevin Buzzard van het Imperial College London, terwijl hij lesgaf aan studenten, vast kwam te zitten omdat Lean eiste dat hij zou bewijzen dat 2 niet gelijk is aan 1. Voor een mens is dit een voor de hand liggende waarheid; voor een formeel logisch systeem is het een fundamenteel feit dat expliciet moet worden gedefinieerd voordat er verdere redenering kan plaatsvinden.
Het overwinnen van deze hindernissen vereiste enorme gezamenlijke inspanningen:
* Enorme digitalisering: In 2018 hebben wiskundigen maanden besteed aan het vertalen van complexe concepten zoals ‘perfectoïde ruimtes’ naar duizenden regels code.
* Gemeenschapsopbouw: Een kleine, toegewijde groep onderzoekers heeft gewerkt om de software gebruiksvriendelijk te maken, door deze van een onhandig academisch hulpmiddel naar een robuust platform te verplaatsen.
* Opschaling: In 2025 was het ecosysteem geëxplodeerd, waarbij tienduizenden gebruikers uit de academische wereld en de technische industrie een bijdrage leverden aan de bibliotheken van Lean.
Waarom dit ertoe doet: de zoektocht naar een ‘waarheidsmachine’
De convergentie van wiskunde en AI is het uiteindelijke doel van deze beweging. Voor software-ingenieurs als De Moura was de prijs een ‘waarheidsmachine’ die kon garanderen dat software als Microsoft Word volledig vrij van bugs is. Voor wiskundigen is het een manier om ervoor te zorgen dat zelfs de meest complexe, abstracte ontdekkingen onberispelijk zijn.
Voor AI-onderzoekers is Lean het ultieme oefenterrein. Door een enorme, geverifieerde bibliotheek met wiskundige waarheden aan te bieden, stelt Lean modellen als AlphaProof in staat om rigoureus redeneren te leren in plaats van alleen maar patroonherkenning. Dit is van cruciaal belang voor het oplossen van het ‘hallucinatie’-probleem bij AI – de neiging van modellen om met vertrouwen valse informatie te geven. Als een AI kan worden getraind om de strikte, onverzettelijke wetten van de wiskundige logica te volgen, kan deze uiteindelijk dezelfde nauwkeurigheid toepassen op redeneren in de echte wereld.
“Zowel [wiskunde als coderen] zijn in exacte syntaxis geschreven als een reeks logische stappen, die elk naar de volgende leiden.”
Conclusie
The Proof in the Code beschrijft hoe een gespecialiseerde tool voor het debuggen van software de basis werd voor een nieuw tijdperk van wiskundige zekerheid en AI-intelligentie. Het benadrukt een diepgaande verschuiving in de wetenschap: de beweging naar een toekomst waarin menselijke intuïtie en digitale verificatie samenwerken om te definiëren wat waar is.
