J.Konstapel.Leiden,19-9-2026

Elke maand halen ze het nieuws. Een advocaat die rechtszaken citeert die nooit hebben bestaan. Een scholier met een keurige literatuurlijst vol verzonnen boeken. Een zoekmachine die met vaste stem een medicijndosering opgeeft die nergens vandaan komt. Het verschijnsel heet hallucinatie.

Dat woord verhult de zaak. Het systeem doet niets fout.

Het doet precies waarvoor het gebouwd is: vloeiende tekst maken.

In de machine bestaat geen grens tussen wat gevonden is en wat gemaakt is. Niet door slordigheid van de bouwers. De grens zit niet in het ontwerp.

Kan dat anders? Kan een AI bestaan waarvan wiskundig vaststaat dat hij niets verzint? Het antwoord is ja. Maar het antwoord zit op een andere plek dan waar iedereen zoekt.

De verkeerde vraag

Het debat over betrouwbare AI gaat over architectuur. Neurale netwerken zouden onbewijsbaar zijn; symbolische systemen bewijsbaar. Dat is de verkeerde as. Bewijsbaarheid is geen eigenschap van de machine. Het is een eigenschap van de bewering die de machine doet.

Vergelijk twee beweringen. De eerste: “dit antwoord is waar over de wereld.” Die bewering heeft geen wiskundige vorm. Er valt niets te bewijzen — voor geen enkele machine, hoe groot ook. De tweede: “dit antwoord staat woordelijk op dit adres in mijn kast, en zo ben ik er gekomen.” Die bewering heeft wél vorm. Die kun je bewijzen. Volledig, voor elke vraag, vooraf.

Het hele verschil tussen onbewijsbare en bewijsbare AI zit in die ene keuze: wat beloof je. De heersende systemen beloven stilzwijgend waarheid en kunnen dat niet waarmaken. Een systeem dat alleen herkomst belooft, kan elke belofte waarmaken.

Waar de grens ligt

Eén ding is principieel onbewijsbaar, en het is precies één ding. Dat een formeel object — een adres, een code — hetzelfde betekent als een zin in gewone taal. Daar zijn twee redenen voor. De eerste is een klassieke stelling van de logicus Alfred Tarski uit 1936: een taal die rijk genoeg is om over zichzelf te spreken, kan haar eigen waarheid niet volledig binnen zichzelf vastleggen. De tweede is alledaagser: gewone taal staat niet stil. Woorden verschuiven met tijd, plaats en spreker. Er is geen vast object om ooit definitief vast te leggen.

De grens is dus geen mist die over alles hangt. Het is één benoemd punt. Alles daarbuiten is gewone wiskunde. Een goed ontwerp is een ontwerp waarin zo min mogelijk — liefst niets — op de verkeerde kant van dat punt staat.

De bibliotheek

Het ontwerp uit het artikel is een bibliotheek. Geen beeldspraak achteraf; zo werkt het letterlijk.

Elk stuk kennis krijgt een adres dat uit de inhoud zelf wordt berekend. Geen catalogus die iemand bijhoudt, geen tabel die geleerd moet worden. Het adres bestaat uit drie tekens: plus, nul, min. Elf posities geven 177.147 vakken. Negentien posities geven ruim een miljard. Wie dieper nummert, maakt oude adressen nooit ongeldig — dat is bewezen: afkappen is afronden, verdiepen is verfijnen.

In de kast ligt alleen wat met een ontvangstbewijs is binnengekomen. Wiskundige stellingen komen alleen binnen met een gecontroleerd bewijs als certificaat. En aan de balie staat een medewerker die maar vier dingen mag: het adres lezen, in het vak kijken, geven wat er ligt — met adres en herkomst erbij — of melden dat het vak leeg is. Verzinnen staat niet in zijn woordenboek. Dat is geen goede bedoeling maar een vorm-eigenschap: het uitvoertype van het systeem kent geen gedaante zonder adres. Een leeg vak heet een vacature, en een vacature is informatie: hier ontbreekt iets, wie vult het.

Let op wat hier wél en niet beloofd wordt. Bewezen is dat de balie niets aflevert dat niet in de kast ligt. Niet bewezen — en nooit bewijsbaar — is dat alles in de kast waar is. Een kast kan een fout boek bevatten. Het systeem verzint niets; dat is de exacte claim, en niets meer.

Wat de mens doet

Eén stap blijft over: van een vraag in gewone taal naar een adres. Dat is precies de onbewijsbare stap van hierboven. Het ontwerp lost dat niet op met doen-alsof. Het systeem stelt voor: dit adres, dit ligt er, dit zijn de buurvakken. De mens beslist.

En die beslissing wordt vastgelegd. Wie, wanneer, welke vraag, welk adres — aaneengeketend, onuitwisbaar. Dat register is geen consensusmachine. Beslissen twee mensen dezelfde vraag verschillend, dan staan er twee vermeldingen, elk met naam en datum. Onenigheid wordt niet weggemiddeld maar zichtbaar bewaard, op één plek. En elke besliste vraag is daarna voorgoed een opzoekvraag: wie hem later stelt, krijgt het vastgelegde adres met het hele spoor erbij. Zo stroomt het onbewijsbare deel — betekenis — vraag voor vraag over in het bewijsbare deel — opzoeken. Bibliotheken van verschillende gemeenschappen zijn samenvoegbaar zonder verbouwing; ook dat is bewezen: samenvoegen is vereniging, er raakt niets kwijt en niets in de war.

Nagerekend, niet betoogd

De kern van dit alles is geen betoog. Hij is uitgeschreven in Lean, een programma dat wiskundige bewijzen controleert. Zeven eigenschappen zijn machinaal gecontroleerd, waaronder: elk getal heeft precies één adres en elk adres rekent terug naar precies één getal; afkappen is afronden; samenvoegen is vereniging; geleverde inhoud staat exact in de kast; een vacature valt alleen bij een werkelijk leeg vak. De computer accepteerde alle bewijzen op niets meer dan de drie standaardaannamen van de gewone wiskunde. Wie het wil nadoen: de bestanden staan in het artikel, de controle duurt een minuut.

Even eerlijk over wat er níét staat. De gecontroleerde kern is klein: de kast is daar een lijst, de balie een directe greep. De productiekast — 3,6 miljoen stukken, publiek toegankelijk — staat nog niet achter de bewezen balie. Twee bewijsverplichtingen staan open. Het artikel bevat een tabel die per eigenschap zegt: bewezen, of alleen gespecificeerd. Die tabel is misschien wel het belangrijkste onderdeel. De meeste AI-teksten hebben zo’n tabel niet, omdat de kolom “bewezen” leeg zou zijn.

Vier machines als recensent

Het artikel is langs vier AI-systemen gegaan voordat het naar een menselijke lezer ging. De eerste ronde vond niets. De tweede sneed raak: de tekst beweerde meer dan de bewijzen droegen. “Kan niet liegen” stond er; bewezen was “kan niets verzinnen” — en dat is niet hetzelfde, want een kast kan een fout antwoord bevatten. Alles is daarop herschreven tot elke bewering exact zo groot is als haar bewijs. De derde ronde vroeg niet om betere tekst maar om werk: grotere kaststructuren, metingen. De vierde herhaalde vooral wat er al stond. Die curve is zelf het resultaat: eerst werd de tekst kleiner, toen werd hij hard. Het stuk zegt nu minder dan de meeste AI-artikelen. En het bewijst meer.

Wat dit niet is, en voor wie het is

Dit is geen concurrent van de vlotte chatbots. De bibliotheek praat niet mooi, redeneert niet vrij, en is trager. Wie een gesprek wil, is bij de grote systemen beter af.

Wie iets anders wil, niet. Een huisartsenpraktijk die haar protocollen vastlegt, weet dat elk antwoord uit de eigen kast komt — of eerlijk “vacature” heet. Een gemeente die besluiten en onderbouwingen adresseert, kan elke bewering herleiden tot stuk, datum en beslisser. Een vakgroep die haar kennis in de kast legt, is er eigenaar van en raakt haar niet kwijt aan een model van een ander. En wie tóch de vlotheid wil: zet een groot taalmodel vóór de balie als voorsteller. Het mag voorstellen wat het wil; alleen wat door de bewezen poort komt, gaat naar buiten. Dan heb je de welbespraaktheid van het ene en de garantie van het andere — en de garantie wint bij elk conflict.

De kern in één zin: betrouwbare AI is geen kwestie van slimmere machines maar van eerlijkere beweringen. Wat een systeem belooft, bepaalt wat je kunt bewijzen. Dit ontwerp belooft weinig, en maakt alles waar.

---

Geannoteerde referenties

1. J. Konstapel, “Provable AI — A Claim-Bounded Criterion, a Semantic Boundary, and a Machine-Checked Construction” (2026). Waarom lezen? Het artikel onder deze blog: het criterium, de grens, het ontwerp, de statustabel en de volledige Lean-bestanden als bijlagen. Leesadvies: wie weinig tijd heeft, leest secties 3–5 en de tabel in sectie 7. — https://claude.ai/artifact/PSG2144zBPND2jQvnfMszE
2. J. Konstapel, “Where Computation Comes From” (2026). Waarom lezen? De voorganger: waarom de moderne rekenmachine zelf al naar berekende adressen, selectie en een minimaal register beweegt. Deze blog bouwt op die vaststelling voort. — https://claude.ai/artifact/2KUPC9w6iqpWM4LxtLZurv
3. J. Konstapel, “The Six Theorems of the MAZE, Second Edition” (2026). Waarom lezen? De zes wiskundige bewijzen onder de bibliotheek — uniek adres, afkappen is afronden, samenvoegen is vereniging — volledig uitgeschreven, stap voor stap. — https://claude.ai/artifact/H5taFTannJ8sTp2de2hueS
4. J. Konstapel, “Waarom de computer verdwijnt” (2026). Waarom lezen? De Nederlandse instap in dezelfde lijn: wat er verdwijnt uit de rekenmachine en waarom. — https://claude.ai/artifact/PsY9nkPtCtnrS7BC4rNqJs
5. A. Tarski, “The Concept of Truth in Formalized Languages” (1936). Waarom lezen? De klassieke stelling achter de grens: waarheid van een rijke taal is niet binnen die taal vast te leggen. De grens in deze blog is toegepaste logica, geen mening. Leesadvies: een moderne samenvatting volstaat; het origineel is zwaar.
6. G. Necula, “Proof-Carrying Code” (1997). Waarom lezen? Het patroon dat hier op antwoorden wordt toegepast: onbetrouwbare producenten, één kleine gecontroleerde poort. Dertig jaar oud en springlevend.
7. G. Klein e.a., “seL4: Formal Verification of an OS Kernel” (2009). Waarom lezen? Het bewijs dat een echt, draaiend systeem end-to-end wiskundig geverifieerd kan worden. De verplichtingen in deze lijn zijn kleiner dan wat seL4 al haalde.
8. P. Lewis e.a., “Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks” (2020). Waarom lezen? De naaste verwant onder de grote systemen: ophalen plus genereren. Het verschil met de bibliotheek is precies één ding — daar blijft de generator het uitvoerpad, hier niet.
9. “Correctness is not Faithfulness in Retrieval Augmented Generation Attributions” (ICTIR 2025). Waarom lezen? Het RAG-veld zelf dat de restkloof benoemt: een correcte citatie is nog geen garantie. Dezelfde vaststelling als deze blog, van binnenuit.
10. Microsoft Research, “BitNet b1.58 2B4T” (2025). Waarom lezen? Het gemeten bewijs dat drie tekens (+1, 0, −1) volstaan als register van een taalmodel, tegen een fractie van de energie. Het register van de bibliotheek is dus geen exotische keuze.
11. D. Knuth, “The Art of Computer Programming”, deel 2 (paragraaf over balanced ternary). Waarom lezen? Knuth noemde het gebalanceerde drietallige stelsel het mooiste talstelsel dat er is. De adresrekening van de bibliotheek staat er kant-en-klaar in.
12. L. de Moura & S. Ullrich, “The Lean 4 Theorem Prover and Programming Language” (2021). Waarom lezen? Het gereedschap waarmee de kern is nagerekend: een taal waarin programma en bewijs samenvallen. Leesadvies: de inleiding volstaat om te begrijpen wat “de computer accepteerde het bewijs” betekent.
13. maze.swarp.nl. Waarom lezen? De draaiende kast: 3,6 miljoen stukken, elk adres een pagina, elke vacature zichtbaar. De productieversie die volgens het werkprogramma achter de bewezen balie moet komen.