Wiskundig bewijs: hoe computers en AI de meest zekere vorm van kennis veranderen
Een wiskundig bewijs is een sluitende redenering die laat zien dat een bewering altijd waar is, zonder enige uitzondering en zonder enige twijfel. Dat is iets anders dan "het klopt in alle gevallen die we hebben getest". Stel je voor dat je duizend dominostenen op een rij zet: als je weet dat steen 1 valt, en je weet zeker dat elke steen de volgende omduwt, dan weet je dat alle duizend stenen zullen vallen. Je hoeft niet te wachten tot steen 1000 ook echt omvalt. Een wiskundig bewijs werkt zo: je begint bij iets wat je als waar aanneemt, en via kleine, controleerbare stapjes toon je aan dat de conclusie wel móet volgen.
Dat maakt wiskunde anders dan natuurkunde of scheikunde. Een natuurwet kan morgen bijgesteld worden door een nieuwe meting, maar de stelling van Pythagoras is al ruim tweeduizend jaar onveranderd waar. Toch is het schrijven en controleren van bewijzen voor moderne, zeer complexe stellingen soms zo omslachtig dat zelfs getrainde wiskundigen fouten maken of het nooit helemaal doorlezen. Daarom wordt er steeds meer gebruikgemaakt van computers en, de laatste jaren, van kunstmatige intelligentie om bewijzen te vinden en te controleren. Dat is het onderwerp van deze pagina.
Wat is het precies?
Een bewijs begint altijd bij axioma's: basisregels die je zonder bewijs aanneemt, omdat je moet beginnen. In de getaltheorie zijn dat bijvoorbeeld de Peano-axioma's over natuurlijke getallen; in bijna de hele moderne wiskunde gebruikt men de axioma's van de verzamelingenleer, afgekort ZFC. Vanuit die axioma's mag je alleen stappen zetten volgens vaste logische regels, zoals: "als A waar is, en A leidt altijd tot B, dan is B ook waar". Elke tussenstap die je zo aflegt, heet een lemma; de keten van lemma's die samen tot de uiteindelijke bewering leiden, is het bewijs, en de bewering zelf heet dan een stelling of theorema.
Er bestaan verschillende bewijstechnieken. Een direct bewijs redeneert rechtstreeks van aanname naar conclusie. Een bewijs uit het ongerijfde (reductio ad absurdum) neemt juist aan dat de bewering onwaar is en laat zien dat dit tot een tegenspraak leidt — dus moet de bewering wel waar zijn. Volledige induktie bewijst iets voor alle natuurlijke getallen door te laten zien dat het geldt voor het eerste getal, en dat het automatisch geldt voor het volgende getal zodra het voor het vorige geldt (de dominoredenering van hierboven). Soms wordt ook de probabilistische methode gebruikt: men bewijst dat iets moet bestaan door aan te tonen dat de kans erop groter is dan nul, zonder een concreet voorbeeld te geven.
Sinds de jaren zeventig spelen computers een rol bij bewijzen die te veel losse gevallen bevatten om met de hand te checken — denk aan duizenden kaartconfiguraties. De laatste tien jaar is daar een nieuwe laag bovenop gekomen: formele bewijsassistenten, computerprogramma's zoals Lean, Coq (recent omgedoopt tot Rocq) en Isabelle. Daarin schrijf je een bewijs niet in gewone taal, maar in een strikte programmeertaal. Een kleine controlekern van het programma checkt dan letterlijk elke stap tegen de logische regels. Als er een fout in zit, accepteert het systeem het bewijs simpelweg niet. Dat is strenger dan een menselijke peer-reviewer, die een fout over het hoofd kan zien.
Wat wil men ermee bereiken?
Het eerste doel is simpelweg zekerheid. Wiskunde vormt de fundering onder natuurkunde, techniek, financiële modellen en cryptografie (de wiskunde achter bankpassen en versleutelde apps). Een fout in een fundamenteel bewijs kan dus, in theorie, ergens anders in de kennisketen problemen veroorzaken. Naarmate bewijzen langer en complexer worden — sommige moderne stellingen hebben bewijzen van honderden pagina's, verspreid over meerdere artikelen van verschillende auteurs — wordt het voor mensen steeds lastiger om alles zelf te controleren.
Een tweede doel is snelheid en samenwerking. Als een bewijs eenmaal in een formele taal is omgezet, kan iedereen ter wereld het laten controleren door de computer, in plaats van te moeten wachten op een select groepje experts dat het vakgebied beheerst. Dat maakt het ook makkelijker om gezamenlijk aan heel grote bewijzen te bouwen, stuk voor stuk, zoals bij een opensourcesoftwareproject.
Een derde, meer toekomstgerichte ambitie is dat kunstmatige intelligentie ooit zelf nieuwe wiskunde kan ontdekken: niet alleen bestaande bewijzen controleren, maar zelf originele bewijsstappen bedenken voor problemen die nog niemand heeft opgelost. Daarnaast hoopt men dat de technieken achter formele bewijzen ook kunnen worden ingezet om kritieke software en hardware — zoals vliegtuigbesturing, chipontwerp of beveiligingsprotocollen — wiskundig gegarandeerd foutloos te maken, in plaats van alleen maar grondig getest.
Voorbeelden uit de praktijk
- Het vierkleurenvermoeden werd in 1976 door Kenneth Appel en Wolfgang Haken bewezen met hulp van een computer, die duizenden kaartconfiguraties doorrekende die met de hand ondoenlijk waren. In 2005 werd dit bewijs door Georges Gonthier volledig geformaliseerd en gecontroleerd in de bewijsassistent Coq.
- Het vermoeden van Kepler over de dichtst mogelijke stapeling van bollen werd in 1998 door Thomas Hales bewezen, maar bevatte zoveel computerberekeningen dat reviewers het niet volledig konden controleren. Het Flyspeck-project formaliseerde het volledige bewijs, en rondde dit in 2014 af met behulp van de bewijsassistenten HOL Light en Isabelle.
- Het Liquid Tensor Experiment (2020-2022) was een uitdaging van Fields-medaillewinnaar Peter Scholze om een van zijn eigen, zeer abstracte stellingen in Lean te formaliseren. Een internationale groep vrijwilligers slaagde daarin, wat liet zien dat ook cutting-edge onderzoekswiskunde geformaliseerd kan worden.
- In 2024 behaalden Google DeepMind's systemen AlphaProof en AlphaGeometry 2 het niveau van een zilveren medaille op de Internationale Wiskunde Olympiade, door opgaven automatisch om te zetten in formele Lean-bewijzen en die vervolgens zelf te vinden.
- Wiskundige Terence Tao gebruikte in 2024 Lean en AI-hulpmiddelen voor het "Equational Theories"-project, waarbij honderden algebraïsche vergelijkingen via massale, deels geautomatiseerde samenwerking werden bewezen of ontkracht.
Hoe ver is de techniek?
Formele bewijsassistenten zijn inmiddels volwassen gereedschap binnen de zuivere wiskunde. De gemeenschapsbibliotheek Mathlib, geschreven in Lean, omvat anno 2025 meer dan een miljoen regels formele code en dekt grote delen van de bachelor- en een deel van de masterwiskunde. Toch is het merendeel van de bestaande wiskunde — zo'n eeuw aan onderzoek — nog niet geformaliseerd; het overzetten gaat gestaag maar langzaam, omdat elk informeel "dat is duidelijk" uit een leerboek in de praktijk vaak tientallen expliciete stappen vereist.
AI-gestuurde bewijsvoering is veelbelovend maar nog smal: systemen als AlphaProof zijn sterk in afgebakende, olympiade-achtige opgaven met een duidelijk juist antwoord, maar nog ver verwijderd van het oplossen van open onderzoeksvragen zoals het Riemann-vermoeden of het P-versus-NP-probleem. Een hardnekkig knelpunt is autoformalisering: het automatisch omzetten van een in gewone taal geschreven wiskundige bewering naar een exacte formele versie, iets waar mensen nog altijd nodig zijn om fouten en dubbelzinnigheden te voorkomen. Ook is er discussie over vertrouwen: een door AI gegenereerd bewijs kan door de bewijsassistent als correct worden afgetekend, maar de onderliggende wiskundige inzichten blijven voor mensen soms ondoorzichtig.
Wie werken eraan?
De bewijsassistent Lean is oorspronkelijk ontwikkeld bij Microsoft Research door Leonardo de Moura en wordt nu verder gebouwd door de onafhankelijke stichting Lean FRO. Coq/Rocq komt van het Franse onderzoeksinstituut INRIA, en Isabelle wordt onderhouden door de universiteiten van Cambridge (VK) en München (Duitsland). Op het gebied van AI zijn vooral Google DeepMind (AlphaProof, AlphaGeometry) en OpenAI actief met wiskundig redenerende modellen.
Aan de academische kant lopen wiskundigen als Terence Tao (UCLA, VS), Peter Scholze (Max Planck Institut, Duitsland) en Kevin Buzzard (Imperial College London, VK, initiatiefnemer van het Xena-project om Lean onder wiskundestudenten te verspreiden) voorop in het formaliseren van onderzoekswiskunde. Instituten zoals het Hoskinson Center for Formal Mathematics aan Carnegie Mellon University en het Clay Mathematics Institute (bekend van de Millennium-prijsvragen) spelen eveneens een rol. Geografisch is het veld geconcentreerd in de VS, het Verenigd Koninkrijk, Frankrijk en Duitsland, met groeiende bijdragen uit China en andere landen via internationale samenwerkingsverbanden.