Elke stelling in een bewijsassistent draagt een exacte, machinaal uitleesbare lijst van de axioma's waarvan haar bewijs afhangt. Dat maakt een vraag meetbaar die in de grondslagen-literatuur meestal kwalitatief blijft: wat kost een axioma? Ofwel: welk deel van de bibliotheek verlies je als je het schrapt? Deze pagina verzamelt de metingen die voor het EEML-programma zijn gedaan, in een vorm die ook los van EEML bruikbaar is voor de bewijsassistent-gemeenschap.
Lean/mathlib: axioma-sluiting per stelling via Lean.collectAxioms over de volledige mathlib-omgeving; aselecte steekproef van 2.000 stellingen uit 439.764 (zaad 137), met binomiale betrouwbaarheidsintervallen. De Diaconescu-splitsing (keuze impliceert in Lean ook de uitgesloten derde) is opgelost door bewijzen te hercompileren tegen een omgeving met alleen klassieke logica zonder getuige-extractie.
Coq/Rocq: volledige telling in plaats van steekproef. Lemma-namen geoogst per module via Search is:Lemma, daarna per lemma de volledige sluiting via Print Assumptions (Coq 8.20.1, alle niet-compat-modules; mathcomp 2.3.0). Primitieve machine-axioma's (63-bits gehelen, floats) zijn apart geteld en niet als logische axioma's geboekt.
Isabelle/HOL: volledige telling over de distributie tot en met Complex_Main (Isabelle2025-2, sessie HOL-Proofs plus eigen audit-sessies met record_proofs = 2): per benoemde stelling de axioma-sluiting via directe traversal van de bewijstermen, met memoisatie over gedeelde deelbewijzen. Conventies: klassiek = True_or_False, keuze = het someI/Eps-axioma, oneindigheid = de Suc_Rep-axioma's, extensionaliteit apart gerapporteerd; definitionele axioma's (typedef) niet geteld. Eerlijke noot: HOL heeft een klassieke kern, dus gemeten wordt "raakt het axioma", exact dezelfde vraag als Leans collectAxioms. De AFP-steekproef gebruikt dezelfde opstelling: twaalf aselecte entries (zaad 20260818, kader: sessie-ouder exact HOL, 318 entries; bouwfalen vervangt per bevroren regel: 19 vervangingen, waarvan 17 bouwfouten), elk als eigen bewijsterm-sessie, met alleen de entry-eigen stellingen geteld.
Alle scripts en zaden zijn gearchiveerd; elke meting is een avond werk om te herhalen. De meetopstelling draait zonder root-rechten (pakketten lokaal uitgepakt).
| Corpus | Omvang | Logisch axioma-gebruik | Detail |
|---|---|---|---|
| mathlib (Lean 4) | 439.764 stellingen (steekproef 2.000) | ~93% gebruikt iets; keuze 70,2% [68,2-72,3] | propext 90,5% · quotiënten 83,7% · echte getuige-extractie ≤ 18,7% · alleen-klassiek ≥ 53,0% · constructieve kern 7,4% |
| Coq-standaardbibliotheek 8.20.1 | 16.664 lemma's (volledig) | 11,5% | klassiek/LPO 11,0% · functie-extensionaliteit 10,5% (beide vrijwel geheel via de klassieke Dedekind-reals) · echte keuze 0,03% · constructief 88,5% |
| mathcomp-analysis 1.9.0 (+ classical, reals) | 5.887 lemma's (volledig) | 77,2% | funext 77,1% · propext 77,1% · keuze-achtig 69,2% · geen LPO · zelfde gemeenschap scoort 0,0% op discreet werk (bevroren continuüm-toets: treffer) |
| Mathematical Components 2.3.0 | 11.442 lemma's (volledig) | 0,0% | ssreflect, eindige groepen, algebra: exact nul axioma's |
| Isabelle/HOL 2025-2 (distributie t/m Complex_Main) | 30.340 stellingen (volledig) | klassiek 88,1% · keuze 44,1% | oneindigheid 46,6% · extensionaliteit 87,8% · discreet 93,7% vs continuüm 92,1% (gradiënt 1,6 punt: uitgewist) · keuze is in HOL een echte keuze |
| Archive of Formal Proofs 2026-08-26 (steekproef 12 entries) | 5.655 stellingen | klassiek 89,2% · keuze 82,0% | oneindigheid 81,9% · discreet 89,2% vs continuüm 89,0% (gradiënt 0,2 punt: uitgewist) · keuze verzadigt in bijgedragen code, anders dan in de distributie |
Prijzen zijn deels stijl, deels onderwerp. Mathlib bewijst met globale klassieke tactieken en betaalt vrijwel overal; mathcomp bewijst vergelijkbare discrete wiskunde (tot en met de machinerie achter de Odd Order-stelling) met exact nul axioma's. Mathlib's 70,2% is dus een bovengrens binnen die bewijsstijl, geen eigenschap van de wiskunde zelf. Deze conclusie is via een vooraf bevroren inzet afgedwongen: de inzet "de prijzen zijn gereedschap-onafhankelijk" is gemeten en gemist, en die mis staat geboekt in het register.
Wat in beide ecosystemen terugkeert, inmiddels als bevroren inzet gemeten en getroffen (13 augustus): axioma-gebruik concentreert zich waar het continuüm binnenkomt. De scherpste vorm staat in de tabel: dezelfde gemeenschap, 0,0% op discreet werk, 77,2% zodra de reële getallen binnenkomen. In Coq zit vrijwel de hele axioma-last bij de reële getallen; de discrete wiskunde is er axioma-vrij. In Lean is de constructieve kern 7,4% en zit de keuze-afhankelijkheid in analyse en topologie. Telbaar is goedkoop, het continuüm is duur.
De derde meting (18 augustus, verwachtingen vooraf bevroren in git): Isabelle/HOL bevestigt de gereedschap-dominantie op zijn scherpst. De discreet/continuüm-gradiënt, in het Coq-ecosysteem ruim 65 punten, is in Isabelle volledig uitgewist: 93,7% tegen 92,1%, een verschil van 1,6 punt, zelfs licht omgekeerd. Als het gereedschap verzadigt, komt het onderwerp-signaal er niet meer doorheen: dat was bevroren verwachting V2, en zij trof. Verwachting V1 (klassiek-raak ≥ 90%) is gemist: het werd 87,6% op het bevroren corpus (88,1% op het uitgebreide), en die mis staat geboekt. De verrassing zit bij keuze: waar in Lean 70,2% aan het keuze-axioma hangt, raakt in Isabelle maar 44,1% de Hilbert-keuze: de klassieke logica verzadigt er wél, het keuze-axioma niet. Drie ecosystemen, drie profielen: de prijzentabel is definitief een gereedschaps-eigenschap.
De AFP-steekproef (dezelfde nacht, drie vooraf bevroren verwachtingen): V3 (klassiek-raak in de band 85-95%) trof op 89,2%. V4 (gradiënt < 20 punten) trof overtuigend: 0,2 punt, nog vlakker dan de distributie. V5 (keuze blijft een minderheid, < 60%) is gemist: door gebruikers bijgedragen entries raken de Hilbert-keuze in 82,0% van de stellingen, bijna het dubbele van de distributie (44,1%). De les: de distributie-kern wordt zuinig gebouwd, maar bijgedragen code leunt vrijwel volledig op de keuze-dragende automatisering en bibliotheek-machinerie. Ook die mis staat geboekt.
Voor bibliotheek-onderhouders (waar zit de axioma-last, en is die nodig?), voor constructieve wiskundigen (welk deel van een corpus is al constructief zonder dat iemand het zo noemde?), en voor iedereen die grondslagen-discussies liever met getallen voert dan met intuïties. Uitbreidingen die voor de hand liggen: het Archive of Formal Proofs (de Isabelle-distributie zelf is inmiddels gemeten), en een jaarlijkse hermeting van mathlib (gepland: augustus 2027, bevroren voorspelling: 70,2% ± 5 punten).
→ context: de Bayes-lezing van axiomakeuze (wiskunde-pagina)