💻 computer science

Auto formalisation of Chaitin and of the surprise incompleteness Theorem

Dit artikel presenteert een casestudy waarbij een LLM (Claude) wordt gebruikt om de autoformalizatie van Chaitins bewijs van de eerste onvolledigheidsstelling en de Kritchman-Raz versie van de tweede onvolledigheidsstelling van de verrassingsexamenparadox in Agda uit te voeren, waarmee het vermogen van het model wordt aangetoond om complexe computationele simulaties te construeren en machine-gecontroleerde bewijzen te produceren, terwijl de huidige sterktes en beperkingen in wiskundige redenering worden belicht.

Oorspronkelijke auteurs: Thierry Coquand

Gepubliceerd 2026-06-12

📖 6 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Thierry Coquand

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Het Grote Plaatje: Een Robot Leren Rekenen

Stel je voor dat je een zeer slimme robot hebt (een AI genaamd Claude) en een zeer strikt, aan regels gebonden wiskundig handboek genaamd "Basic Recursive Arithmetic". Dit handboek is als een spel met zeer specifieke regels: je mag alleen basisrekenen en eenvoudige logica gebruiken, geen flauwekul of "magische" trucjes.

Het doel van dit artikel is om te zien of de robot een complexe, beroemde wiskundige bewijsvoering (over waarom wiskunde grenzen heeft) kan lezen en deze volledig kan herschrijven in de strikte taal van dat handboek, zonder dat een mens ook maar één regel code schrijft.

Het antwoord is ja. De robot slaagde erin om twee diepe wiskundige ideeën te vertalen naar deze strikte taal, waarbij hij een bewijs creëerde dat een computer kan controleren op 100% juistheid.

De Twee Hoofdzieën

Het artikel richt zich op twee beroemde concepten: Chaitins Bewijs (gerelateerd aan de eerste onvolledigheidsstelling) en de Verrassingsexamen-paradox (een versie van de tweede onvolledigheidsstelling).

1. Het "Korte Beschrijving" Spel (Chaitins Bewijs)

Stel je voor dat je een bibliotheek hebt van elke mogelijke verhaal die je zou kunnen schrijven met een beperkte set letters.

De Regel: Sommige verhalen zijn heel kort en makkelijk te beschrijven. Andere zijn zo complex dat de kortste manier om ze te beschrijven is door simpelweg het hele verhaal op te schrijven.
Het Probleem: Chaitins bewijs probeert een verhaal te vinden dat zo complex is dat het niet door een kort programma beschreven kan worden.
De Uitdaging voor de Robot: Om dit te bewijzen, moest de robot binnen het wiskundige handboek een "machine" bouwen die een verhaal kan lezen, het kan uitvoeren en kan zien wat het doet.
De Hindernis: Het wiskundige handboek is te simpel om van nature "het draaien van een programma" af te handelen, omdat dat meestal een complexe functie vereist (zoals de Ackermann-functie) die het handboek niet toestaat.
De Oplossing: De menselijke auteur suggereerde een truc genaamd "Gandy/Howard majorisation". Denk hierbij aan het geven van een brandstoftank aan de robot. In plaats van de machine te vragen om eeuwig door te gaan, berekent de robot precies hoeveel "brandstof" (stappen) een programma nodig heeft om klaar te zijn. Het bouwt een speciale "brandstofmeter" die garandeert dat het programma stopt voordat de tank leeg is.
Het Resultaat: De robot bouwde deze brandstofmeter uit zichzelf. Het bewees dat als je probeert een getal te beschrijven dat "te complex is om eenvoudig te worden beschreven", je een logische tegenstrijdigheid creëert (zoals bewijzen dat 0 gelijk is aan 1).

2. Het "Verrassingsexamen" en de Hoop Zand

Het tweede deel van het artikel behandelt een beroemde paradox: Een docent kondigt aan dat er volgende week een verrassingsexamen zal zijn. De studenten redeneren dat het niet vrijdag kan zijn (want als ze tegen donderdag nog niets hebben gehoord, weten ze dat het vrijdag is), dus kan het ook geen donderdag zijn, enzovoort... totdat ze concluderen dat er helemaal geen examen kan zijn. Maar dan geeft de docent het examen op woensdag, en is het een verrassing.

Het artikel gebruikt een versie van deze logica (door Kritchman en Raz) om te bewijzen dat een wiskundig systeem niet zijn eigen consistentie kan bewijzen (dat het geen tegenstrijdigheden bevat).

De Oude Manier: Eerdere bewijzen telden het aantal dagen of getallen om een tegenstrijdigheid te vinden.
De Nieuwe Manier (De Sorites/Hoop Zand Paradox): De auteurs vergelijken dit met de Paradox van de Hoop Zand.
- Als je een hoop zand hebt en je verwijdert één korrel, is het nog steeds een hoop.
- Als je er nog een verwijdert, is het nog steeds een hoop.
- Als je korrels één voor één blijft verwijderen, eindig je uiteindelijk bij nul korrels. Maar op welk exact punt was het geen "hoop" meer?
De Toepassing:
- Stel je een lijst met getallen voor van 0 tot een enorm groot getal $N$ .
- De logica probeert te bewijzen: "Het is onmogelijk dat alle deze getallen een korte beschrijving hebben."
- De robot bewijst dit stap voor stap. Het zegt: "Als we aannemen dat getallen 0 tot en met $N$ allemaal een korte beschrijving hebben, krijgen we een tegenstrijdigheid."
- Daarna verwijdert het 0. "Oké, als 1 tot en met $N$ korte beschrijvingen hebben, krijgen we nog steeds een tegenstrijdigheid."
- Het blijft één getal tegelijk verwijderen (zoals het verwijderen van korrels zand).
- Uiteindelijk bereikt het een punt waar de lijst leeg is, maar de logica dwingt toch een tegenstrijdigheid af.
De Twist: Het artikel betoogt dat dit geen "vicieuze cirkel" van zelfverwijzing is; het is meer zoals de hoop zand. Je kunt één korrel (één getal) veilig weghalen, maar als je het blijft doen, stort de hele structuur in. Deze instorting bewijst dat het wiskundige systeem niet kan bewijzen dat het veilig is (consistent) zonder zichzelf te breken.

Waarom Dit Belangrijk Is (Volgens het Artikel)

AI als Wiskundige Assistent: Het artikel laat zien dat huidige AI (zoals Claude) nu goed genoeg is om de kleine, saaie details van complexe wiskundige bewijzen af te handelen. Het kan parsers bouwen, machines evalueren en logische stappen afhandelen die mensen normaal gesproken handmatig moeten doen.
Constructieve Wiskunde: Het artikel benadrukt dat in de "constructieve wiskunde" (waar je daadwerkelijk het ding moet bouwen waar je over praat), het idee van een "partiële functie" (een programma dat misschien eeuwig blijft draaien) lastig is. De robot moest een "loopend" programma gebruiken dat misschien eeuwig blijft draaien, maar het bewijs garandeert dat het stopt. Dit is een subtiel maar cruciaal onderscheid dat de AI correct afhandelde.
Geen Magische Trucs: De robot gebruikte geen "tactics" (snelkoppelingen) of fancy bibliotheken. Het bouwde alles vanaf nul met alleen de basisregels van het wiskundige systeem. Dit maakt het bewijs zeer robuust en gemakkelijk te verifiëren door een computer.

De Conclusie

Het artikel is een casestudy die aantoont dat AI nu kan fungeren als een krachtige partner in de formele wiskunde. Het kan een hoog niveau idee (zoals "wiskunde heeft grenzen") nemen en dit vertalen naar een rigide, machine-controleerbaar formaat.

De auteurs merken op dat hoewel de AI een mens nodig heeft om het te begeleiden (zoals het suggereren van de "brandstoftank"-truc), de AI vervolgens autonoom de code kan schrijven, de logica kan opbouwen en het hele proces kan documenteren. Het resultaat is een volledig geverifieerd bewijs dat verheldert hoe deze diepe logische paradoxen precies werken, waarbij ambiguïteit wordt weggestreept en alleen de harde, logische feiten overblijven.

Technische Samenvatting: Automatische Formalisering van Chaitin en de Verrassingsonvolledigheidstelling

Probleem en Context
Dit rapport breidt een vorig experiment uit met betrekking tot de auto-formalisering van de tweede onvolledigheidsstelling van Gödel met behulp van het large language model (LLM) Claude en de bewijsassistent Agda. Het primaire doel is om de capaciteiten en beperkingen van huidige LLM's te onderzoeken bij het formaliseren van complexe wiskundige bewijzen, specifiek diegene die betrokken zijn bij de interne representatie van berekening. Het artikel richt zich op twee specifieke doelen: Chaitins bewijs van de eerste onvolledigheidsstelling en de Kritchman-Raz "verrassingsexamenparadox"-versie van de tweede onvolledigheidsstelling.

Een centrale technische uitdaging die wordt aangepakt, is de codering van berekening binnen Basic Recursive Arithmetic (BRA), een systeem (geformuleerd door Guard) dat geen object-kwantoren en standaard tactieken bezit. In een dergelijk systeem is het definiëren van een interne evaluatiefunctie onmogelijk, omdat dit de primitief recursieve grenzen zou overschrijden (vergelijkbaar met de Ackermann-functie). Het probleem vereist het representeren van programma's en hun executiestappen volledig binnen de objecttaal, zonder te vertrouwen op meta-niveau functies of externe bibliotheken.

Methodologie
Het project hanteert een "spartanse" aanpak waarbij geen enkele regel Agda-code door de menselijke auteur is geschreven; de formalisering werd autonoom gegenereerd door Claude op basis van hoogwaardige wiskundige beschrijvingen. De methodologie steunt op de volgende technische strategieën:

Ternaire String-codering: Programma's worden gerepresenteerd als natuurlijke getallen die geïnterpreteerd worden als ternaire strings (digitale 1, 2, 3). Dit maakt het mogelijk om de verzameling programma's van lengte maximaal $L^*$ te behandelen als een eenvoudig initieel segment van natuurlijke getallen $\{p < N\}$ , waarbij $N = 3^{L^*+1}$ , wat complexe enumeratiemechanismen vermijdt.
CK Machine Implementatie: Om de noodzaak voor een globale evaluatiefunctie te omzeilen, heeft Claude autonoom een continuation stack small-step evaluatiemachine (een Landin CK machine) geconstrueerd. Deze machine deelt expressies op en beheert een stack van continuaties, waardoor berekeningen stap voor stap gesimuleerd kunnen worden.
Gandy/Howard Majorisatie: Een cruciale hindernis was het bewijzen dat de machine binnen een specifiek aantal stappen stopt voor een gegeven functie $f$ binnen de logica. Omdat het aantal stappen geen meta-niveau natuurlijk getal kan zijn, hebben de auteurs Claude begeleid om de Gandy/Howard majorisatie methode te gebruiken. Dit houdt in dat een gesloten combinator fuel(f) via primitieve recursie wordt gedefinieerd die de werkelijke looptijd van $f$ bewijsbaar majoriseert. Dit maakt het mogelijk om de volledigheid van de interpreter intern binnen BRA te formuleren en te bewijzen.
Verrassingsexamen als Sorites: Het bewijs van de tweede onvolledigheidsstelling vermijdt de telargumenten die door Kritchman en Raz worden gebruikt. In plaats daarvan modelleert het argument de argumentatie als een Sorites (hoop zand) paradox. Het procedureert via externe inductie op een stadium $r$ , waarbij wordt bewezen dat het onmogelijk is dat alle getallen in het interval $[r, N]$ korte beschrijvingen hebben.

Belangrijkste Bijdragen en Resultaten
Het artikel presenteert een volledig door machine gecontroleerd bewijs in Agda van de volgende resultaten voor Church's Basic Recursive Arithmetic:

Auto-geformaliseerde Chaitins Stelling: Het systeem heeft succesvol Chaitins bewijs geformaliseerd, dat de Liar-zin vervangt door Kolmogorov-complexiteit. De formalisering produceert een expliciete bewijs-transformator $G$ . De stelling stelt dat als een term $w$ een bewijs codeert van de oncomprimeerbaarheidsaussage $K(out(w)) > L^*$ , dan codeert $G \cdot w$ een bewijs van $0=1$ . Dit wordt geformuleerd als een positieve object-niveau implicatie in plaats van een meta-theoretische negatie van bewijsbaarheid.
Geïnternaliseerde Tweede Onvolledigheid: Het artikel formaliseert het Kritchman-Raz argument om aan te tonen dat als $T$ zijn eigen consistentie ( $Con_T$ ) bewijst, dan $T$ inconsistent is ( $0=1$ ). Het bewijs verloopt via een daling van $S(0)$ (het duiventilprincipe) naar $S(N+1)$ (een contradictie), waarbij elke stap $S(r) \to S(r+1)$ de consistentiehypothese precies één keer consumeert.
Constructieve Inzichten: De formalisering benadrukt de rol van partiële functies in constructieve wiskunde. Specifiek enumereert het diagonale programma afleidbare formules totdat een doel wordt gevonden. Hoewel het programma extern bewezen wordt te termineren, wordt de grootte ervan berekend zonder de terminatiebewijzen te internaliseren. Dit demonstreert een manifestatie van het Blum speed-up fenomeen, waarbij het toestaan van een partiële recursieve functie (die extern totaal wordt gehouden) leidt tot onbeperkt kortere programma's vergeleken met die welke intern moeten certificeren dat ze stoppen.

Betekenis en Claims
Het artikel claimt dat huidige coderende LLM's, zoals Claude, effectieve instrumenten zijn voor het begrijpen van de granulaire details van wiskundige papers, mits zij opereren onder constante supervisie. Het project dient als een casestudy die aantoont dat:

LLM's autonoom complexe syntactische machinerie (parsers, evaluatiemachines) en logische argumenten (majorisatie) kunnen genereren wanneer zij worden gestuurd door hoogwaardige structurele hints.
Type theory (specifiek Agda zonder tactieken) zeer geschikt is voor het uitdrukken van concrete wiskunde die betrekking heeft op berekening en codering, aangezien bewijzen direct gerepresenteerd kunnen worden zonder behoefte aan functionele extensionaliteit of quotient types.
Het "verrassings"-argument, wanneer het geformaliseerd wordt, nauwer aansluit bij de Sorites-paradox dan de traditionele verrassingsexamenparadox, aangezien de contradictie voortvloeit uit de iteratie van geldige stappen in plaats van een enkele zelf-referentiële lus.

De auteurs concluderen dat de taal van type theory perfect is voor deze combinatorische, computationele wiskunde, maar dat een belangrijke onderzoeksvraag overblijft: hoe ontwerpen we formele systemen die in staat zijn om niet-combinatorische objecten met een vergelijkbare automatisering te behandelen. De formalisering verheldert impliciete details in de oorspronkelijke presentaties van Chaitin en Kritchman-Raz en biedt een rigoureuze, door machine geverifieerde fundering voor deze argumenten binnen een minimaal rekenkundig kader.