🔢 mathematics

Proof by Mechanization: Cubic Diophantine Equation Satisfiability is $Σ^0_1$ -Complete

Deze paper bewijst dat de bevredigbaarheid van een enkele Diophantische vergelijking van graad 3 over de natuurlijke getallen $\Sigma^0_1$ -compleet en dus onbeslisbaar is, door een uniform primitief recursief compiler te construeren die arithmetische zinnen omzet in dergelijke vergelijkingen en dit resultaat volledig te mechaniseren in Rocq.

Oorspronkelijke auteurs: Milan Rosko

Gepubliceerd 2026-03-09

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Milan Rosko

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

Stel je voor dat wiskunde een enorme, eindeloze bibliotheek is. In deze bibliotheek staan boeken met raadsels. Sommige raadsels zijn makkelijk op te lossen, zoals "wat is 2 + 2?". Andere raadsels zijn zo complex dat niemand ooit zeker kan weten of er een oplossing bestaat, of dat het raadsel gewoon onoplosbaar is.

Dit artikel van Milan Rosko gaat over een heel specifiek soort raadsel: Diophantische vergelijkingen. Dat klinkt eng, maar het zijn gewoon vergelijkingen waarin je alleen hele getallen (zoals 1, 2, 3...) mag gebruiken om de vraag op te lossen.

De grote vraag die dit artikel beantwoordt is: Hoe ingewikkeld moet zo'n vergelijking zijn voordat het onmogelijk wordt om te weten of er een oplossing bestaat?

Hier is de uitleg, vertaald naar alledaagse taal:

1. De "Legpuzzel" van de Wiskunde

Stel je een vergelijking voor als een legpuzzel.

Niveau 1 (Lineair): Dit is als een rechte lijn leggen. "Ik heb 3 appels en 2 peren, hoeveel fruit heb ik?" Dit is makkelijk.
Niveau 2 (Kwadratisch): Dit is als een vierkant maken. "Ik heb een stukje grond, de oppervlakte is 100, wat zijn de afmetingen?" Dit is nog steeds oplosbaar met slimme wiskundige trucs.
Niveau 3 (Kubisch): Dit is als een kubus (een doosje) bouwen. "Ik heb een doosje met een volume van 1000, wat zijn de afmetingen?"

Voor een lange tijd wisten wiskundigen dat als je vergelijkingen heel ingewikkeld maakt (bijvoorbeeld graad 4 of hoger), je nooit meer zeker kunt weten of er een oplossing is. Maar bij graad 2 was het wel zeker. Graad 3 was het "grijze gebied": niemand wist zeker of het hier al onoplosbaar werd.

2. De Grootte van de Bibliotheek (Het Aantal Variabelen)

Het artikel zegt niet alleen dat graad 3 lastig is, maar dat het onmogelijk is om een algemene regel te vinden die voor elke kubische vergelijking zegt of er een oplossing is.

Het is alsof je een supercomputer hebt die alle mogelijke legpuzzels moet controleren. De auteurs bewijzen dat er een punt is waarop deze computer vastloopt. Het maakt niet uit hoe slim de computer is; voor bepaalde kubische vergelijkingen kan hij nooit zeggen: "Ja, er is een oplossing" of "Nee, er is geen oplossing". Hij blijft voor eeuwig doorgaan met zoeken.

3. De "Vertaler" (De Compiler)

De auteurs hebben een heel slimme machine gebouwd, een soort vertaler.

Input: Je geeft de machine een bewijs uit de logica (een redenering of een stelling).
Output: De machine vertaalt dit bewijs direct naar een kubische vergelijking.

De magische regel is: Als het bewijs klopt, dan heeft de vergelijking een oplossing. Als het bewijs niet klopt, dan heeft de vergelijking geen oplossing.

Omdat we weten dat er in de logica bewijzen zijn waarvoor we nooit kunnen weten of ze kloppen (dit is een beroemd resultaat van Gödel), betekent dit automatisch dat er ook kubische vergelijkingen zijn waarvoor we nooit kunnen weten of ze een oplossing hebben.

4. De "Magische Doos" (De Universele Vergelijking)

Het meest indrukwekkende deel is dat ze niet alleen zeggen "het bestaat", maar dat ze een concrete, fysieke vergelijking hebben gemaakt.
Stel je een enorme, ingewikkelde formule voor met bijna 10.000 variabelen (zoals 10.000 verschillende vakjes die je moet invullen). Deze ene formule is een "universele sleutel".

Als je er een specifiek getal in stopt, wordt het een raadsel dat overeenkomt met het vraagstuk "Is deze stelling waar?".
Als je een ander getal erin stopt, wordt het een ander raadsel.

Ze hebben deze formule gebouwd, de getallen erin gecontroleerd door een computer (Rocq), en bewezen dat hij echt werkt. Het is alsof ze een enkele, gigantische sleutel hebben gesmeed die elk slot in de wiskundige bibliotheek kan openen, maar die zelf zo complex is dat niemand de sleutel kan analyseren om te zien of hij werkt zonder hem te proberen.

5. Waarom is dit belangrijk? (De "Wachtrij")

De auteurs gebruiken een mooie analogie met een wachtrij.

Bij simpele vergelijkingen (graad 1 en 2) kun je snel zien wie er aan de beurt is.
Bij graad 3 wordt de wachtrij zo lang en ingewikkeld dat je niet meer kunt voorspellen of iemand eruit komt.

Ze tonen aan dat de grens tussen "oplosbaar" en "onoplosbaar" precies op graad 3 ligt. Het is het moment waarop wiskunde zijn eigen grenzen bereikt. Het is het punt waarop de logica zo diep wordt dat je niet meer van buitenaf kunt kijken of er een oplossing is; je moet erin duiken, en als je erin duikt, loop je vast.

Samenvatting in één zin

De auteurs hebben bewezen dat er een enkele, enorme kubische vergelijking bestaat die zo complex is dat het oplossen ervan precies even moeilijk is als het vinden van een antwoord op elke mogelijke vraag in de wiskunde, en dat we daarom nooit een algemene methode kunnen vinden om te zeggen of zo'n vergelijking een oplossing heeft.

Het is een bewijs dat de wiskunde, net als het universum, bepaalde geheimen heeft die voor altijd verborgen blijven voor onze rekenmachines.

1. Probleemstelling

Het artikel adresseert een langdurig open probleem in de getaltheorie en de berekenbaarheidstheorie: de beslissingscomplexiteit van Diophantische vergelijkingen.

Achtergrond: Volgens het MRDP-theorema (Matiyasevich, Robinson, Davis, Putnam) is het beslissingsprobleem voor Diophantische vergelijkingen over de natuurlijke getallen ( $\mathbb{N}$ ) onbeslisbaar (het is $\Sigma^0_1$ -volledig).
Bestaande kennis:
- Graad 2: Vergelijkingen van graad 2 zijn deels beslisbaar (via klassieke getaltheoretische methoden).
- Graad 4: Jones (1980) toonde aan dat elke recursief oprekenbare verzameling de oplossingsverzameling is van een Diophantische vergelijking van graad 4 met 58 variabelen.
- Graad 3: De status van vergelijkingen van graad 3 was onbekend. Bestaande reducties van graad 4 naar graad 3 vereisten een "zwarte doos" aanpassing die de graad niet lokaal controleerde of resulteerde in systemen met een onbeperkt aantal variabelen, zonder een enkele vergelijking te genereren.
De Kernvraag: Is de satisfiability (oplosbaarheid) van een enkele Diophantische vergelijking met graad $\le 3$ over $\mathbb{N}$ onbeslisbaar?

2. Methodologie

De auteur gebruikt een geautomatiseerde, mechanische aanpak ("Proof by Mechanization") om een bewijs te leveren dat volledig is geverifieerd met het bewijsassistentie-systeem Rocq (een variant van Coq). De methode bestaat uit drie conceptuele lagen:

A. Register Arithmetic (RA) en Arithmetisering

De auteur definieert een zwak formeel systeem, Register Arithmetic (RA), gebaseerd op $I\Delta_0 + B\Sigma_1$ maar beperkt tot de taal zonder vermenigvuldiging ( $L_{RA} = \{0, S, +, =\}$ ).
Vermenigvuldiging wordt niet als primitief gebruikt, maar als een $\Sigma_1$ -relatie gedefinieerd via iteratieve optelling.
Syntax en bewijzen in dit systeem worden gearchiveerd (arithmetized) naar natuurlijke getallen.

B. De Compiler (Proof-to-Polynomial)

Er wordt een uniforme, primitief-recurseve compiler $\phi \mapsto S_\phi$ ontworpen. Deze compiler vertaalt de code van een bewijs in RA naar een stelsel van Diophantische vergelijkingen.
Graadcontrole:
- Syntactische checks en het verifiëren van bewijsstappen (axioma-matching, modus ponens) worden vertaald naar kwadratische vergelijkingen (graad $\le 2$ ).
- De "Guard"-mechanisme: De enige bron van termen van graad 3 ontstaat wanneer een lineaire selectievariabele (graad 1) een kwadratische verplichting activeert (bijv. $a_i \cdot Q(\vec{x}) = 0$ ).
- Er worden geen kwadratische termen vermenigvuldigd met andere kwadratische termen, waardoor de graad nooit boven 3 uitkomt.
Carryless Pairing: Om complexe datastructuren (zoals bewijstraces) in Diophantische vergelijkingen te coderen zonder "dragen" (carry propagation) die de graad zou verhogen, maakt de auteur gebruik van Zeckendorf-voorstellingen in het Fibonacci-basisstelsel. Dit zorgt voor een injectieve, draagloze koppelingsfunctie.

C. Aggregatie naar één Vergelijking

Het compileren resulteert eerst in een stelsel van vergelijkingen. Om dit om te zetten in één enkele vergelijking zonder de graad te verhogen (zoals bij som-van-kwadraten, wat graad verdubbelt), gebruikt de auteur een mixed-radix aggregatie methode.
Elke vergelijking $A_i = B_i$ wordt behandeld als een "digit" in een groot getalsysteem. Door gewogen sommen te nemen met een basis $B$ (bepaald door Fibonacci-getallen), wordt het stelsel samengevoegd tot één vergelijking $\sum B^i A_i = \sum B^i B_i$ .
Capaciteitsbeperkingen (via Lagrange's vier-kwadraten stelling) zorgen ervoor dat de variabelen binnen de juiste "digit" grenzen blijven, waardoor de gelijkheid van de som impliceert dat elke individuele vergelijking geldt.

3. Belangrijkste Bijdragen

Eerste Constructie van een Universele Graad-3 Vergelijking: Het artikel presenteert een expliciete, effectief gegenereerde universele Diophantische vergelijking van graad 3.
- De auteur geeft een concrete coefficiententabel voor een dergelijke vergelijking met 9.692 variabelen (in de definitieve constructie).
- Dit lost het open probleem op dat door Jones (1980) en Gasarch (2021) werd geïdentificeerd.
Mechanisch Geverifieerd Bewijs: Het volledige bewijs, inclusief de correctheid van de compiler, de graadgrenzen en de equivalentie tussen bewijsbaarheid en oplosbaarheid, is geïmplementeerd en geverifieerd in Rocq. Er zijn geen axioma's of "Admitted" (ongeverifieerde) stappen gebruikt.
Lokaal Graadcontrole: In tegenstelling tot eerdere "zwarte doos" reducties, toont dit werk aan dat de graad van 3 lokaal wordt bereikt door een specifiek syntactisch mechanisme (selector $\times$ kwadratische check) en niet door een globale, oncontroleerbare transformatie.
Bounded Universality: Het artikel introduceert het concept van "bounded universality": voor elke begrensde resource-parameter $k$ (bijv. bewijslengte) bestaat er een specifieke, beslisbare graad-3 vergelijking die precies de waarheid van bewijzen binnen die grens vastlegt. De onbeslisbaarheid ontstaat door de unie over alle $k$ .

4. Resultaten

$\Sigma^0_1$ -Volledigheid: Het artikel bewijst dat het probleem $HN(3, n)$ (oplosbaarheid van een enkele Diophantische vergelijking van graad 3 met $n$ variabelen, waarbij $n$ deel uitmaakt van de input) $\Sigma^0_1$ -volledig is.
Onbeslisbaarheid: Als gevolg hiervan is het beslissingsproblem voor enkele Diophantische vergelijkingen van graad 3 over $\mathbb{N}$ onbeslisbaar.
Diagonaal Argument: Door de Diagonaalstelling toe te passen op de compiler, wordt aangetoond dat er geen totale Turing-machine bestaat die de satisfiability van deze vergelijkingen correct kan beslissen zonder een contradictie met Gödels Tweede Onvolledigheidsstelling te creëren (als RA consistent is).
Concrete Artifacts: De auteurs publiceren concrete coefficiententabellen (in JSON/OCaml) die door de Rocq-kernel zijn geverifieerd op graad $\le 3$ en integriteit.

5. Betekenis en Impact

Sluiting van een Gaten in de Getaltheorie: Dit werk sluit de kennislacune tussen de beslisbare kwadratische gevallen en de onbeslisbare kwartische gevallen. Het bevestigt dat graad 3 de kritieke drempel is voor onbeslisbaarheid in Diophantische vergelijkingen.
Verbinding tussen Bewijstheorie en Algebra: Het toont een directe, mechanische link tussen de logica van zwakke arithmetische systemen en de algebraïsche structuur van polynomen. Het bewijs dat "bewijsbaarheid" exact kan worden vertaald naar "oplosbaarheid van een graad-3 polynoom".
Methodologische Vooruitgang: Het gebruik van mechanisatie (Rocq) voor dit type fundamentele onmogelijkheidsresultaten is baanbrekend. Het elimineert de kans op menselijke fouten in complexe, technische reducties die decennia lang hebben bestaan.
Impredicativiteit van de Grens: De auteur concludeert dat de grens van onbeslisbaarheid inherent "impredicatief" is; om de graad-3 drempel te definiëren, moet men de mechanismen gebruiken die de onbeslisbaarheid zelf veroorzaken (zelfreferentie via de diagonaalstelling).

Kortom, dit artikel levert het eerste rigoureuze, mechanisch geverifieerde bewijs dat de satisfiability van enkele Diophantische vergelijkingen van graad 3 onbeslisbaar is, en biedt een concrete, uitvoerbare constructie van een universele dergelijke vergelijking.