Dit is een vervolg op The Great Dreams of Alexander Grothendieck.
Grothendieck’s Prophecy: From Dreams to Resonant Computing
maar ook op The Chemical Origin of Semantic Intelligence.
Introductie
Het intuïtionisme is een stroming in de wiskunde uit de jaren 30 van de 2ode eeuw, die plotseling dominant wordt in de computerkunde vanwege de type-theorie, een gevolg van een mislukte poging van Bertrand Russell en Ludwig Wittgenstein om de wiskunde te formaliseren.
De oorzaak is een onoplosbare paradox die wordt veroorzaakt door het getal oneindig, wat eigenlijk geen getal (tellen) is, maar een onmogelijkheid, omdat de mens eindig is.
Brouwer (Intuïtionisme) eiste dat wiskundige objecten constructief bewezen moesten worden door middel van een eindig stappenplan.
Dat lukt nooit met oneindige verzamelingen.
Oneindige verzamelingen kun je wel beperken tot potentieel oneindig door het maximum te binden aan een vaste grens.
Een wiskundig bewijs toont de lange draden, die “logisch” op elkaar volgen van begin tot het einde.
Ze tonen een enorm landschap wat de wiskunde op den duur hoopt te overdekken.
De vanzelfsprekendheid van de gekozen afslag hangt af van het persoonlijke geloof in de goede richting die weer afhangt van de persoonlijkheid, die weer vertrouwt op regels, eigen waarneming (feiten), de waardering van anderen en het innerlijke zicht wat weer afhangt van de levensloop..
Deze Blog gaat Over wat de Waarheid is en Was in de Wiskunde.
1. Van Euclides tot Hilbert: bewijs als deductie uit axioma’s
Euclides: het klassieke beeld
Met Euclides’ Elementen (ca. 300 v.Chr.) ontstaat het standaardbeeld:
- je kiest axioma’s en definities,
- je leidt daaruit stellingen af,
- met bewijzen die stap voor stap “noodzakelijk volgen”.
Tot ver in de 19e eeuw is dit het ideaal: wiskunde als een axiomatisch netwerk met bewijs als formele rechtvaardiging van stellingen.
In de 19e eeuw ontstaan spanningen:
analysetechnieken blijken slordig (oneindige reeksen, limieten);
nieuwe geometrieën (niet-Euclidisch) laten zien dat axioma’s niet vanzelfsprekend zijn;
Cantors verzamelingen en paradoxen in de naïeve verzamelingenleer bedreigen consistentie.
Reactie:
Weierstrass en anderen maken analyse ε-δ-strikt;
Hilbert werkt aan formele axiomatiseringen (geometrie, later ook fundamenten van de wiskunde).
Hilberts “programma” (ca. 1920) is duidelijk:
Formaliseer alle wiskunde in een formeel systeem en bewijs met redeneren dat dat systeem consistent is.
Gödel: scheiding tussen waarheid en bewijs
Gödel (1931) laat zien: dat een systeem zichzelf niet kan beschrijven.
Je hebt iets anders nodig om het verschil te kunnen bemerken.
- in elk voldoende sterk consistent formeel systeem bestaan ware maar onbewijsbare uitspraken;
- dus: “waar” en “formeel bewijsbaar” vallen niet samen.
Dat blijft tot vandaag een basis-spanningsveld:
- logici werken met modellen en waarheid (Tarski),
- proof-theoretici en intuïtionisten met bewijzen en afleidbaarheid.
2. 20e eeuw: meerdere, concurrerende opvattingen van bewijs
Brouwer en het intuïtionisme
Brouwer stelt dat concepten in de wiskunde voorstelbaar moeten zijn.
Dit resulteert in de afwijzing van oneindig als bewijsmiddel, omdat een mens eindig is en dus nooit zeker weet dat stap n+1 na stap n al komt, net zoals een oneindigheid een tegendeel heeft.
- Wiskunde is een mentale constructie door een “scheppend subject”.
- Een uitspraak is alleen waar als er een concrete constructie/bewijs voor gegeven kan worden.
- De wet van het uitgesloten derde (
P ∨ ¬P) wordt op oneindige domeinen afgewezen als er geen constructie is.
Hier wordt bewijs primair: waarheid = bestaan van een bewijs (in de zin van een constructie).
Deze lijn wordt later geformaliseerd in intuïtionistische logica en Martin-Löfs type-theorie, waar “propositie = type” en “bewijs = term van dat type”.
HOTT
Gentzen’s Logica
Proof theory en model theory
Parallel ontstaan twee grote formele tradities:
- Proof theory (Gentzen):
- bewijzen zelf worden object van studie (sequent calculus, cut-elimination, normalisatie);
- je analyseert de vorm van bewijzen om de sterkte van systemen te begrijpen.
- Model theory (Tarski):
- logische geldigheid = “waar in alle modellen”;
- focus op structuren waarin uitspraken waar/vals zijn.
Later komt daar proof-theoretic semantics bij (Dummett, Prawitz, Schroeder-Heister), waar de betekenis van logische connectieven wordt gedefinieerd via hun rol in bewijzen (intro-/eliminatieregels), niet via waarheidswaarden in modellen.
Kort: er is geen één “officiële” definitie van bewijs meer; er zijn meerdere compatibele maar concurrerende perspectieven.
Lakatos en de praktijk: bewijs als proces
Met Imre Lakatos’ Proofs and Refutations (1960s/1976) verschuift de focus naar de werkelijke praktijk:
- stellingen beginnen als ruwe conjectures,
- bewijzen worden gepresenteerd,
- tegenvoorbeelden dwingen aanpassing van zowel bewijs als stelling,
- het geheel is een dialectisch proces van “proofs and refutations”.
Bewijs is hier:
- niet alleen een eindproduct,
- maar een instrument in een iteratief onderzoeksproces,
- ingebed in een gemeenschap die accepteert, corrigeert, verfijnt.
Murawski en co.: formeel vs informeel bewijs
Recente overzichten, zoals Murawski’s “Proof vs Truth in Mathematics” (2021), maken expliciet onderscheid tussen:
- informele bewijzen: de teksten/argumenten zoals wiskundigen die schrijven en lezen;
- formele bewijzen: strikte objecten in een formeel systeem (metastructuur).
Belangrijk:
- informele bewijzen zijn vaak gappy, vertrouwen op “het is duidelijk dat…”;
- formele bewijzen zijn volledig checkbaar maar meestal enorm en onleesbaar.
De relatie tussen die twee is nu een kernonderwerp: hoe verhouden “bewijs als mensen het doen” en “bewijs zoals een machine het controleert” zich?
3. Proof assistants en formeel bewijzen (1970–2020)
De Bruijn tot Coq, Isabelle, Lean
Vanaf eind jaren 60 ontstaan proof assistants:
- Automath (de Bruijn) als vroege poging om wiskunde in een computer-leesbare taal te coderen; motivatie: groeiende behoefte aan formeel verifieerbare bewijzen.
- Later systemen: Mizar, HOL, Coq, Isabelle, HOL Light, Lean, enz.
Kenmerken:
- gebaseerd op hoger-orde logica of (afhankelijke) type-theorie;
- kleine, betrouwbare kernel die bewijzen checkt (de Bruijn-criterium);
- grote bibliotheken (Archive of Formal Proofs, mathlib, Mathematical Components, etc.).
Grote formele successen
Een paar mijlpalen:
- Feit–Thompson (Odd Order Theorem):
zes jaar werk in Coq; volledige mechanische verificatie van een zeer complexe groepsbewijstheorie. - Kepler-conjectuur (Flyspeck):
combinatie van HOL Light en Isabelle; formele bevestiging van Hales’ proof over dichtste bolverpakkingen. - Industrie:
verificatie van de seL4-microkernel, CompCert-compiler en formele specificaties bij o.a. Amazon Web Services.
State of the art rond 2015–2020:
- formele bewijzen zijn mogelijk voor zeer complexe stellingen,
- maar zijn duur, specialistisch, en vragen intensieve menselijke inzet,
- filosofisch: het bestaan van zulke bewijzen versterkt de status van “formele bewijs = goudstandaard” – maar roept de vraag op wat begrip betekent als bijna niemand het formele bewijs kan “lezen”.
4. 2020s: AI, LLMs en neuro-symbolische bewijssystemen
De laatste vijf jaar is er een duidelijke verschuiving naar AI-ondersteund bewijzen.
AlphaGeometry: olympiad-niveau in meetkunde
AlphaGeometry (DeepMind, 2024):
- neuro-symbolische architectuur: een neuraal taalmodel + een symbolische deductie-engine,
- lost 25 van 30 historische IMO-meetkundeproblemen op binnen wedstrijdtijd, vergelijkbaar met een gemiddelde gouden medaillewinnaar.
Het systeem genereert formele meetkundige bewijzen, niet alleen antwoorden.
AlphaProof: IMO-niveau in algebra/NT/combinatoriek
AlphaProof (DeepMind):
- koppelt een grote taalmodus (Gemini) aan AlphaZero-achtige reinforcement learning en de Lean-proof assistant;
- transformeert een IMO-probleem naar Lean-tactieken, en gebruikt search + RL om een formeel bewijs te vinden, automatisch gecheckt in Lean.
Resultaat:
- op de IMO 2024 loste het systeem drie van de vijf niet-meetkundige problemen op, inclusief het moeilijkste probleem;
- samen met AlphaGeometry 2 werd vier van de zes problemen opgelost, goed voor een score van 28/42 punten → silver-medaille-niveau.
Beperkingen nu:
- uren tot dagen rekentijd per probleem,
- menselijk expert moet problemen nog vertalen naar formele taal,
- geen “begrip” zoals mensen dat bedoelen – maar rigoureuze, machine-gecheckte bewijzen zijn er wel.
Brede trend: LLM + proof assistant
Daarnaast verschijnen systemen als:
- DeepSeek-Prover: RL op basis van Lean-feedback zodat een LLM beter formele bewijzen kan construeren.
- LeanProgress: model dat voorspelt hoe ver je in een bewijs bent, gebruikt om proof search efficiënt te sturen.
- studies over hoe LLMs effectief in verificatie-pipelines kunnen worden ingeschakeld.
Kort: de state of the art nu is een hybride:
- AI genereert lemma’s, proof-stappen, tactieksequenties,
- een proof assistant checkt alles strikt,
- mensen gebruiken dit als co-pilot bij formalisatie en probleemoplossen.
5. Conceptuele stand van de discussie vandaag
Heel grof zie je nu vier lijnen naast elkaar lopen:
- Formele lijn
- Proof theory, type-theorie, proof assistants;
- bewijs = formele afleiding / object in een formeel systeem;
- AlphaProof past hier naadloos in.
- Constructieve lijn (Brouwer, Martin-Löf)
- bewijs = constructie;
- AI-systemen in constructieve proof assistants (Coq/Lean) leveren letterlijke programma’s als bewijzen.
- Praktijk/sociaal (Lakatos, Hersh, Mancosu, Murawski)
- bewijzen zijn ook sociale artefacten;
- de rol van vertrouwen, “gappy proofs”, stijl en uitleg is expliciet onderwerp van onderzoek.
- AI-lijn
- bewijs als co-product van mens + machine;
- nieuwe vragen: wat betekent “ik begrijp het bewijs” als een groot deel door AI gegenereerd is? Is een AI-bewijssketen van 10.000 stappen die niemand handmatig naloopt, maar wel formeel gecheckt is, “even goed” als een kort menselijk bewijs?
Murawski en anderen zien expliciet dat de kloof tussen informele en formele bewijzen nu gevuld wordt door proof assistants en AI: informele bewijzen worden steeds vaker auto-geformaliseerd, en formele bewijzen worden weer samengevat in leesbare argumenten.
6. Verre toekomst: wat gaan AlphaProof-achtige tools veroorzaken?
Nu het interessante deel: strategische implicaties. Dit is uiteraard deels speculatief, maar ik baseer het op wat we nu al zien in de literatuur en in praktijkprojecten.
6.1. Van bewijs als tekst → bewijs als pipeline
De richting is duidelijk:
- Informele stelling (natuurtaal)
→ autoformalisation (LLM + menselijke correctie)
→ proof search (AlphaProof-achtig)
→ formeel bewijs in proof assistant
→ automatisch gegenereerde menselijke samenvatting + visualisatie.
Als dit doorzet, krijg je:
- Bewijs = pipeline van tools, niet één lineair argument.
- Elk deel van de pipeline is log- en data-gedreven; je kunt terugspoelen, varianten testen, dependencies analyseren.
Strategisch gevolg:
- tijdrovend “lemma-chasing” en zoeken naar combinatorische case-splitsingen wordt commodity;
- de schaarste verschuift naar:
- kiezen van goede definities,
- formuleren van vruchtbare conjectures,
- architectuur van theorieën.
6.2. Nieuwe rol van de menselijke wiskundige
Als AlphaProof-achtige systemen veel standaardproblemen kunnen oplossen, zie je waarschijnlijk:
- Mens als architect, AI als uitvoerder
- mens: kiest concepten, definities, modellen, frameworks;
- AI: vult details in, zoekt counterexamples, formaliseert, verfijnt.
- architectuur + kritieke stukken door senior engineers,
- veel boilerplate door tooling.
- Scheiding tussen “verification proof” en “understanding proof”
- “verification proof”: lang, formeel, door machine gecheckt → veiligheid, zekerheid;
- “understanding proof”: korter, conceptueler, gericht op inzicht.
- machine-bewijs garandeert correctheid,
- mensen schrijven aparte “explanatory proofs” als leer- en communicatiemiddel.
- Verschuiving in wat als “prestige” geldt
- nu: prestige zit sterk op “eerste correct bewijs”;
- straks: prestige mogelijk meer op:
- bedenken van nieuwe concepten/axioma’s,
- ontwerpen van proof-pipelines,
- bouwen van grote, coherente formalisatie-ecosystemen.
6.3. Onderwijs en selectie
Met krachtige AI-bewijshulp verandert ook onderwijs:
- Basiscasus:
- studenten gebruiken proof assistants + AI om hun bewijzen te checken;
- docenten verschuiven naar het beoordelen van structuur, model-keuze, uitleg in plaats van hver afzonderlijke stap.
- Selectie:
- olympiades en examens zullen moeten bepalen in hoeverre AI is toegestaan;
- wellicht ontstaan aparte tracks:
- “pure human performance”,
- “human+AI collaboration”.
Gevolg: klassieke “bewijs-training” (handmatig epsilon-delta, eindeloze inductie-oefeningen) wordt minder belangrijk als skill op zich, en meer een middel om intuïtie en kwaliteit van modellering te ontwikkelen.
6.4. Institutionele veranderingen
Concrete scenario’s:
- Journal-policies
- voor complexe resultaten kan een tijdschrift gaan eisen:
- óf een formeel bewijs in een erkende proof assistant,
- óf ten minste een machine-controle van kernstappen.
- voor complexe resultaten kan een tijdschrift gaan eisen:
- Nieuwe rollen
- “formalization engineers” of “proof engineers” als erkende rol in onderzoeksgroepen;
- aparte credits voor:
- het ontwikkelen van formalisatie-infrastructuur,
- het toepassen van AI-bewijstools op bestaande conjectures.
- Data- en tool-soevereiniteit
- grote formeel-bewijslibraries (mathlib, AFP, etc.) worden kritieke infrastructuur;
- vragen rond licenties, openheid en controle:
- wié bezit de proof-data?
- mag een commerciële partij een private fork maken van de hele wiskundige kennisbasis?
6.5. Nieuwe typen risico en “onveiligheid”
AlphaProof-achtige systemen lossen één type risico op:
- hallucinaties van pure LLMs → mitigatie door formele verificatie.
Maar er komen nieuwe risico’s bij:
- Model-/formeel-mismatch
- het formele systeem modellleert de wiskunde goed,
- maar de link “natuurtaal → formeel probleem” is fout of incompleet;
- je krijgt dan een perfect bewijs van de verkeerde stelling.
- Tool-keten-kwetsbaarheid
- bug in de kernel van een proof assistant,
- fout in de integratie tussen AI-agent en prover,
- onopgemerkte inconsistentie (Girard-achtige issues in een te krachtig type-systeem als de implementatie fouten bevat).
- Overbetrouwbaarheid op black-box AI
- als een lab alles via één gesloten AI-stack formaliseert, bouw je een single point of failure in de kennis-infrastructuur.
Antwoord hierop zal bijna zeker zijn:
- meerdere onafhankelijke proof assistants,
- auditing-tools die proofs tussen systemen vertalen,
- best-practices vergelijkbaar met “defence in depth” in security.
6.6. Lange-termijn filosofische verschuivingen
Een paar plausibele bewegingen:
- Normalisering van “onmenselijk grote bewijzen”
- nu al heb je bewijzen die alleen door kleine teams en over jaren echt gecheckt worden (stelling van de eindige eenvoudige groepen, Feit–Thompson, Flyspeck);
- met AI wordt het normaal dat niemand het hele bewijs lineair kan begrijpen, maar we vertrouwen het omdat:
- het formeel gecheckt is,
- meerdere pipelines hetzelfde resultaat geven.
- Herwaardering van “proof-theoretic semantics”
- als bewijzen massaal door machines worden gegenereerd, wordt de vorm van bewijzen en hun proof-regels nóg belangrijker;
- discussies over betekenis via bewijzen (in plaats van modellen) worden praktischer: je kunt empirisch kijken naar grote proof-corpora.
- Nieuwe grens tussen bewijs en experiment
- als AI miljoenen proof-pogingen, varianten en “counterexample-searches” uitvoert, wordt de scheidslijn tussen bewijs en computational experiment vager;
- voor sommige gebieden (dynamische systemen, grote combinatoriek) zouden we stellingen kunnen accepteren op basis van:
- een formeel bewezen “meta-stelling”,
- plus massaal empirisch AI-onderzoek binnen die meta-grenzen.
- Menselijke “geloofslaag” blijft bestaan
- uiteindelijk zal elke gemeenschap (wiskundigen, ingenieurs, financiers van onderzoek) moeten bepalen welke combinatie van menselijk inzicht en machine-bewijs zij voldoende vindt;
- dat is precies die laag van waardering en geloof waar je eerder zelf op wees: regels en feiten zijn niet genoeg, er is altijd een beslissingslaag die zegt “dit accepteren we”.
7. Slot
Samengevat:
- Historisch is het begrip “bewijs” geëvolueerd van Euclidische deductie via Hilbert-formaliteit, Brouwer-constructie en Lakatos-dialoog naar een situatie waar we bewijzen tegelijk zien als:
- formele objecten,
- cognitieve constructies,
- sociale producten,
- en nu ook computationele artefacten.
- De state of the art vandaag:
- grote formele libraries,
- proof assistants in industriële en wiskundige toepassingen,
- AI-systemen zoals AlphaProof/AlphaGeometry die op IMO-niveau opereren met formeel gecheckte bewijzen.
- Vooruitkijkend zullen AlphaProof-achtige tools het veld verschuiven naar:
- bewijzen als pipelines,
- mensen als architecten en interpreten,
- onderscheid tussen zekerheid (machine-bewijs) en begrip (menselijke uitleg),
- nieuwe instituties, risico’s en governance rond de bewijzinfrastructuur zelf.