💻 logic

Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound

Dit artikel sluit een kritiek verificatiegat in de minimale Kochen–Specker-grens door exacte rationale case-tree-certificaten en twee onafhankelijke checkers (één in Python en één formeel bewezen in Lean 4) te introduceren om de geometrische niet-inbedbaarheid van alle 180 onderscheidende grafen in de gepubliceerde blocking-database machinaal te verifiëren, waardoor ongeverifieerde Z3-beslissingen worden vervangen door door de kernel gecontroleerde stellingen, terwijl tegelijkertijd verschillende verborgen gebreken en discrepanties in de oorspronkelijke bewijspijplijn worden ontdekt en opgelost.

Oorspronkelijke auteurs: Shayaan Siddique, Ibrahim Mian

Gepubliceerd 2026-07-29

📖 6 min leestijd🧠 Diepgaand

Oorspronkelijke auteurs: Shayaan Siddique, Ibrahim Mian

✨ 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 je probeert een huis te bouwen van onzichtbare, magische blokken. In de wereld van de kwantumfysica worden deze blokken "vectoren" genoemd, en ze hebben een zeer vreemde regel: als twee blokken onder een perfecte rechte hoek ten opzichte van elkaar staan, kunnen ze niet beide tegelijkertijd "aan" staan. Dit is de kern van het Kochen–Specker-theorema, een beroemd idee dat bewijst dat het universum niet slechts een gigantische, voorspelbare machine is waarbij elk onderdeel een vooraf ingestelde geheime schakelaar heeft. In plaats daarvan suggereert het dat de handeling van het kijken naar een kwantumsysteem bepaalt hoe het zich gedraagt.

Decennialang spelen natuurkundigen een spel met hoge inzet van "hoe klein kunnen we dit maken?". Ze willen de kleinste mogelijke verzameling van deze magische blokken vinden die een tegenstrijdigheid creëert — een situatie waarin de regels van het spel het onmogelijk maken om "aan" of "uit" staten toe te wijzen zonder de natuurwetten te breken. Het huidige record voor de kleinste bekende verzameling is 31 blokken. Maar de grote vraag is: wat is het absolute minimum? Zou het kunnen met 25? 24? Of zelfs minder?

Om dit te beantwoorden, gebruiken onderzoekers krachtige computerprogramma's om duizenden potentiële blokarrangementen te genereren en vervolgens te proberen te bewijzen dat geen van deze arrangementen daadwerkelijk in onze 3D-wereld kan bestaan. Het is als een detective die probeert te bewijzen dat een verdachte het misdrijf niet gepleegd kan hebben door aan te tonen dat hun alibi wiskundig onmogelijk is. Het probleem is dat, voor het moeilijkste deel van dit bewijs, de vorige detectives moesten vertrouwen op een "black box" computeroplosser. Ze vroegen de computer: "Is dit arrangement mogelijk?" en de computer zei: "Nee." Maar de computer toonde niet zijn werk, waardoor er een klein gat in de logica ontstond waar een fout zich kon verbergen.

Dit artikel gaat over het dichten van dat gat. De auteurs, Shayaan Siddique en Ibrahim Mian, besloten een nieuw soort "bewijs van ontvangst" te bouwen voor elk afzonderlijk onmogelijk arrangement. In plaats van alleen op het "Nee" van de computer te vertrouwen, creëerden ze een stapsgewijs, wiskundig perfect certificaat dat iedereen (of elke andere computer) kan controleren om het resultaat te verifiëren. Ze controleerden niet slechts één of twee; ze controleerden 291 specifieke gevallen (die 180 unieke vormen vertegenwoordigen) die de basis vormen van de huidige beste ondergrens: 24 vectoren.

Hier is hoe ze het deden en wat ze vonden:

Het Magische Bewijs
Stel je voor dat je probeert te bewijzen dat een specifieke vorm bestaande uit blokken niet kan bestaan. De oude manier was om een superintelligente AI te vragen, die getallen zou verwerken en zou zeggen: "Onmogelijk." De nieuwe manier, uitgevonden in dit artikel, is om de AI te vragen een verhaal te schrijven. Dit verhaal is een "case-tree certificaat". Het begint met een paar basisblokken en vertakt zich vervolgens als een "kies je eigen avontuur"-boek. Bij elke splitsing in de weg legt het verhaal uit waarom een bepaalde route tot een tegenstrijdigheid leidt.

De auteurs maakten deze verhalen ongelooflijk rigoureus. Ze gebruikten "exacte rationale rekenkunde", wat betekent dat ze geen benaderingen of gissingen gebruikten (zoals zeggen "dit is ongeveer 3,14"). In plaats daarvan gebruikten ze perfecte breuken. Als het verhaal zegt dat een getal nul is, dan is het exact nul, niet "bijna nul". Ze bouwden twee onafhankelijke "controleurs" — één geschreven in Python en één in een formele bewijstaal genaamd Lean 4 — om deze verhalen te lezen. Deze controleurs zijn als strikte bibliothecarissen die elke stap van het verhaal verifiëren. Als het verhaal een typefout of een logische sprong bevat, wijst de bibliothecaris het af.

De Verrassingen in de Bibliotheek
Toen de auteurs de oude "black box"-resultaten begonnen te lezen met hun nieuwe, strikte controleurs, vonden ze enkele verrassingen die de oorspronkelijke onderzoekers hadden gemist omdat ze te veel op de computer vertrouwden.

De "Distinctness" Valstrik: Het oorspronkelijke computerprogramma ging ervan uit dat elk afzonderlijk blok in de verzameling uniek moest zijn, zelfs als ze elkaar niet aanraakten. De auteurs ontdekten dat voor sommige vormen de enige reden dat ze "onmogelijk" waren, was omdat twee blokken per ongeluk hetzelfde blok waren geworden. Als je die regel zou versoepelen, zou de vorm misschien wel werken! Dit betekende dat het oorspronkelijke bewijs vertrouwde op een verborgen regel over "injectiviteit" (erop toezien dat dingen verschillend zijn) die niet even voor de hand lag.
Verborgen Doodlopende Wegen: De computeroplosser sloeg soms "degeneratieve" gevallen over — vreemde, randgevallen waarbij de wiskunde rommelig wordt. De nieuwe certificaten dwongen de auteurs om deze rommelige gevallen expliciet uit te schrijven, waarmee ze bewezen dat de vormen zelfs in de vreemdste hoeken nog steeds niet konden bestaan.
Telfouten: Het oorspronkelijke artikel beweerde dat er 41 definitieve kandidaatvormen overbleven om te controleren. De nieuwe, rigoureuze herhaling van de data toonde aan dat er er eigenlijk 43 waren. Het blijkt dat de oorspronkelijke telling er twee te ver naast zat. Hoewel dit het grote plaatje niet verandert (de grens is nog steeds 24), laat het zien dat we zonder deze perfecte bewijzen misschien twee belangrijke puzzelstukjes hadden gemist.

Het Resultaat
Het artikel certificeert succesvol dat 180 verschillende geometrische vormen (afkomstig uit 291 regels data) niet in onze 3D-wereld gebouwd kunnen worden. Ze deden dit door de ongeverifieerde "black box"-antwoorden te vervangen door 291 geverifieerde, door machines controleerbare certificaten.

Ze bewezen ook dat 42 van de 44 definitieve kandidaten voor het minimum aantal vectoren kunnen worden uitgesloten omdat ze een van deze gecertificeerde onmogelijke vormen in zich bevatten. Dit laat slechts 2 kandidaten over die nog onbewezen zijn, maar nu weten we precies wat het zijn, en de weg naar het bewijs van deze kandidaten is helder.

De auteurs zeiden niet alleen: "We denken dat het 24 is." Ze bouwden een systeem waarbij elke stap een gesloten, logische lus is die door een computer in ongeveer een halve seconde kan worden gecontroleerd. Ze veranderden een "vertrouw ons"-argument in een "toon je werk"-argument. Hoewel het definitieve bewijs dat het absolute minimum exact 24 is (en niet 23) nog enkele onderdelen nodig heeft om volledig te worden samengesteld, heeft dit artikel de geverifieerde basis gelegd voor de geometrische helft van de puzzel. Het bewijst dat voor de overgrote meerderheid van de gevallen het universum deze vormen inderdaad verbiedt, en we hebben nu de bewijzen om dat aan te tonen.

Technische Samenvatting: Door de machine gecontroleerde certificaten voor de geometrische helft van de minimale Kochen–Specker-grens

Probleemstelling

Het minimale Kochen–Specker (KS) probleem zoekt het kleinste aantal $n$ niet-nul vectoren in $\mathbb{R}^3$ , paarwijze verschillend als stralen, zodanig dat hun orthogonaliteitsgraaf geen $\{0, 1\}$ -kleuring toelaat waarbij elk orthogonaal paar maximaal één $1$ bevat en elk orthogonaal triade exact één $1$ bevat. De best bekende ondergrens is $n \ge 24$ , vastgesteld door computationele methoden door Li et al. en Kirchweger et al.

Dit bewijs bestaat uit twee helften:

Combinatorische helft: Een isomorf-vrije SAT-enumeratie van kandidaat-grafen tot orde 23. Onvervulbaarheidscresultaten worden vergezeld door DRAT-bewijzen, die onafhankelijk controleerbaar zijn.
Geometrische helft: Een demonstratie dat elke geënumereerde kandidaat-graaf niet-inbedbaar is in $\mathbb{R}^3$ . Deze helft vertrouwt op de nonlinear real arithmetic (NRA) solver van Z3 om te bepalen dat geen enkele toewijzing van niet-nul, straal-distincte vectoren aan de orthogonaliteitsvoorwaarden voldoet.

De kritieke kloof die in dit werk is geïdentificeerd, is dat de geometrische helft geen controleerbare bewijsobjecten produceert. De vertrouwensketen eindigt in de beslissingsprocedure van Z3 voor een $\exists\mathbb{R}$ -harde theorie, waardoor de gemeenschap de oordelen over niet-inbedbaarheid op basis van geloof moet accepteren. Bovendien vertrouwt de gepubliceerde pipeline op "blocking databases" van minimale niet-inbedbare subgrafen, die eveneens door Z3 zijn afgeleid en ongeverifieerd zijn.

Methodologie

De auteurs introduceren een framework voor het genereren en verifiëren van exacte rationale case-tree certificaten voor reële niet-inbedbaarheid. De methodologie vervangt de opake Z3-beslissingsprocedure door een transparant, algebraïsch verificatieproces.

1. Certificaatstructuur
Een certificaat is een op zichzelf staand object bestaande uit:

Anker en Propagatie: Een normalisatiestap (het verankeren van een orthogonaal triade of rand) gevolgd door een propagatieschema dat alle vertex-vectoren uitdrukt in termen van enkele parameters met behulp van kruisproducten en vlak-parametrisaties.
Case Tree: Een boomstructuur waarbij interne knopen splitsingen vertegenwoordigen op basis van:
- Factorisatie: $p = \prod f_k$ , geverifieerd door expansie.
- Som van kwadraten (SOS): $p = \sum c_k m_k^2$ met $c_k \in \mathbb{Q}_{>0}$ , geverifieerd door expansie.
Bladeren: Takken worden gesloten door een van vier mechanismen:
- Injectiviteitsbotsing: Bewijzen dat twee verschillende vertices naar parallelle stralen mappen.
- Verplichtingsinstorting (Obligation Collapse): Laten zien dat een vereiste niet-nul polynoom identiek nul is.
- Ideaal lidmaatschap: Expliciete cofactoren die bewijzen dat een polynoom deel uitmaakt van het ideaal gegenereerd door de restricties.
- Positivstellensatz-vormige positiviteit: Een gegeneraliseerd argument dat laat zien dat een som van positieve termen (injectie-polynomen) gelijk is aan een som van kwadraten, wat leidt tot een contradictie bij reële punten.

2. Verificatiearchitectuur
Het systeem maakt gebruik van twee onafhankelijke checkers die geen enkele code delen met de certificaatgenerator:

Pure-Python Replay: Voert de certificaatlogica uit met behulp van exacte rationale rekenkunde.
Lean 4 Total Checker: Een reflectieve functie Cert.check geïmplementeerd in de Lean 4 proof assistant.
- Kernel-reduceerbaarheid: Om te garanderen dat het oordeel een gesloten kernel-stelling is, hebben de auteurs een gcd-vrije rationale rekenkundelaag (KRat) en fuel-structural recursie geïmplementeerd. Dit maakt het mogelijk dat de gehele berekening wordt gereduceerd door de Lean-kernel zonder native reductie of aangepaste axioma's.
- Axioma-sluiting: De deugdelijkheidstelling vertrouwt enkel op {propext, Classical.choice, Quot.sound}, waardoor ongeverifieerde native reducties worden vermeden.

3. Deugdelijkheidstelling (Soundness Theorem)
De kernstelling, check_sound, stelt dat als check c = true, er geen realisatie van de graaf bestaat. Een realisatie wordt gedefinieerd als een afbeelding naar $\mathbb{R}^3$ die voldoet aan niet-nul vectoren, orthogonaliteit op randen, en paarwijze straal-distinctheid (injectiviteit) voor alle vertex-paren.

Belangrijkste Bijdragen

Exacte Rationale Certificaten: De introductie van een certificaatformaat dat numerieke benaderingen en opake solvers vervangt door exacte rationale rekenkunde, polynoomfactorisaties en SOS-decomposities.
Volledige Dekking van de Blocking Database: Certificering van alle 291 bronregels (die 180 verschillende grafen vertegenwoordigen) uit de gepubliceerde PhysicsCheck blocking lijsten (ordes 10–13), waarbij elk Z3-oordeel wordt vervangen door een door de machine gecontroleerde stelling.
Duale Onafhankelijke Replay: Validatie door twee verschillende checkers (Python en Lean) die 115 vijandige mutaties (bijv. gemanipuleerde coëfficiënten, verwijderde takken) verwerpen terwijl ze echte certificaten accepteren.
Formalisatie-gestuurde Bevindingen: De rigoureuze formalisatie onthulde specifieke problemen in de oorspronkelijke pipeline:
- Injectiviteit is Cruciaal: De oorspronkelijke Z3-codering dwong paarwijze straal-distinctheid af voor alle paren, niet alleen voor aangrenzende paren. Verschillende grafen in de database zijn enkel niet-inbedbaar vanwege deze injectiviteitsrestrictie, een nuance die onzichtbaar is voor standaard geometrische solvers.
- Verborgen WLOG-gevallen: De orthoplane-parametrisatie die in de oorspronkelijke pipeline werd gebruikt, verborg degeneratieve gevallen (parallelle vectoren) die expliciet moeten worden afgehandeld door injectie-argumenten.
- Empirische Optimalisatie: Een "niet-kleurbaarheid" optimalisatie in de oorspronkelijke pipeline bleek empirisch te zijn in plaats van een fundamentele stelling.
- Reproduceerbare Aantallen: De gepubliceerde telling van de uiteindelijke orde-23 kandidaten (41) bleek niet reproduceerbaar uit de artefacten; het correcte aantal is 43, waarvan er 42 zijn afgehandeld door de nieuwe orde-13 certificaten.

Resultaten

Verificatie Dekking: Alle 180 verschillende grafen in de blocking database hebben nu gesloten kernel-stellingen die hun niet-inbedbaarheid bewijzen.
Prestaties: Kernel-evaluatie kost ongeveer 0,5 seconden voor orde-10/11/12 grafen en 1,8 seconden voor orde-13 grafen op een standaard laptop. De volledige verificatiesuite draait binnen enkele minuten.
Impact op de Grens: De zeven nieuwe orde-13 certificaten handelen 42 van de 44 uiteindelijke kandidaten in de orde-22/23 enumeratie af via geverifieerde subgraph-monotoniciteit. De overige twee kandidaten worden bijgehouden als expliciete, machine-leesbare verplichtingen.
Adversarial Robuustheid: Beide checkers wezen alle 115 gemuteerde certificaten succesvol af tijdens continuous integration, wat aantoont dat de verificatielogica niet louter een replay is van de output van de generator, maar een echte onafhankelijke controle.

Betekenis

Het artikel claimt de vertrouwenskloof te dichten voor de geometrische helft van de minimale KS-grens met betrekking tot de blocking database. Door ongeverifieerde Z3-oordelen om te zetten in gesloten kernel-stellingen, zorgt het werk ervoor dat de niet-inbedbaarheid van de kritieke subgrafen niet langer een kwestie is van geloof in een black-box solver.

De auteurs benadrukken dat het formalisatieproces zelf een primaire bron van waarde was, waarbij verborgen aannames (injectiviteit), verborgen geval-verplichtingen en datadiscrepanties aan het licht kwamen die onzichtbaar waren voor de oorspronkelijke workflow. Hoewel het artikel nog geen volledig geverifieerde end-to-end stelling voor $n \ge 24$ vormt (vanwege de schaal van de SAT-enumeratie en de bewijzen van canonicaliteit), legt het de geverifieerde geometrische basis en biedt het een schaalbaar pad vooruit. Het werk demonstreert dat complex geometrisch redeneren in kwantumfundamenten volledig machine-controleerbaar kan worden gemaakt met exacte rekenkunde en minimale axioma's.