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

Ibrahim Mian; Shayaan Siddique

REVIEW 2 major objections 5 minor 15 references

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

T0 review · 2 major / 5 minor · reviewed 2026-08-01 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Machine-checked certificates now close the geometric half of the 24-vector Kochen-Specker lower bound.

desk verdict Genuinely useful formal-verification work that closes the uncheckable Z3 gap on the KS blocking database; the main residual risk is the unverified parser bridge from published files to certified graphs. read the letter →

arxiv 2607.26413 v1 pith:TXOULYRV submitted 2026-07-29 cs.LO quant-ph

Shayaan Siddique , Ibrahim Mian This is my paper · ORCID

classification cs.LOquant-ph MSC 03B3568V2014P1005C62

keywords Kochen-Speckertheoremvectorsystemsnon-embeddabilitycertificatesexactrationalarithmeticsum-of-squaresproofsmachine-checkedproofassistantsgraphrealizability

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper claims to close the main trust gap in the best known lower bound for the minimum Kochen-Specker vector system: the part that showed candidate graphs cannot be embedded in R^3. The published proof relied on a nonlinear real arithmetic solver that returned answers without checkable evidence. The paper introduces exact rational case-tree certificates, each encoding a WLOG normalization, a propagation schedule, and a finite case analysis whose leaf proofs are polynomial factorizations and rational sum-of-squares identities. Two checkers, one standalone and one inside a machine-checked proof assistant, replay the certificates with no shared code, and the soundness theorem behind the proof-assistant checker is kernel-verified. The paper argues that acceptance by that checker implies no injective-on-rays, orthogonality-respecting assignment of nonzero real vectors realizes the graph, so every one of the 291 source lines (180 distinct graphs) in the pipeline's blocking lists now has a closed machine-checked non-embeddability theorem.

What carries the argument

The central object is the rational case-tree certificate: a self-contained document recording an anchor, a propagation schedule, a parameter list, and a finite case tree. The tree's nodes split on polynomial factorizations (over an integral domain, a product zero forces a factor zero) and rational sum-of-squares identities (over a formally real field, a sum of squares zero forces each term zero); leaves close branches by injectivity collisions, ideal membership with explicit cofactors, or a Positivstellensatz-shaped positivity identity involving products of pair-injectivity polynomials. The work it does is to reduce real non-embeddability to identities checked by exact rational arithmetic, s

What would settle it

Independently search for a realization of any graph that the checker accepts: if any nonzero, pairwise ray-distinct vectors in R^3 satisfy all edge orthogonalities, the soundness theorem would be inconsistent. A simpler first test is to feed the checker a known-embeddable graph and require rejection, and to rerun the published filter on the pinned hashes to check the reported 43/44 candidate count.

Watch

Extended reading notes

Core claim

The central claim is that for every graph in the published blocking database, non-embeddability in R^3 can be witnessed by a finite, exact-rational object whose correctness is independently decidable. Each certificate anchors a triad or edge to basis vectors, replays a schedule of cross-product and plane-parametrization steps that expresses all vertex vectors as polynomials in a few parameters, and presents a case tree. Internal splits are factorization or sum-of-squares identities checked by expansion; leaves are discharged by injectivity collisions, obligation collapse, ideal membership with explicit cofactors, or a Positivstellensatz-shaped positivity argument. Because the checker is prov

Load-bearing premise

The whole chain transfers to the published Kochen-Specker bound only if the 291 source lines and the filter semantics from the original pipeline were transcribed exactly; if the parse, pinning, or candidate replication is wrong, the certificates prove non-embeddability of graphs other than the pipeline's actual candidates.

Editorial extensions

If this is right

If correct, the geometric half of the lower-bound proof no longer depends on trusting a nonlinear real arithmetic solver; every blocking graph's non-embeddability is independently replayable and kernel-checked.
The seven order-13 certificates discharge 42 of the 44 final candidates through verified subgraph monotonicity, so the path to a fully verified bound of at least 24 is reduced to two unresolved candidates plus the remaining layers of encoding correctness, canonicity, and streaming SAT proof replay.
The same certificate format should transfer to other real-algebraic non-embeddability problems where the obstruction is real-geometric rather than purely algebraic, since leaves can speak about positivity and injectivity loci.
The findings about the published pipeline show that building proof objects can surface discrepancies, such as an unreproducible candidate count and hidden case obligations, that are invisible to solver-trusting workflows.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

A natural next step beyond this paper is to produce direct certificates for the two remaining final candidates, since the verified chain currently carries them as explicit hypotheses rather than closed theorems.
The certificate format's reliance on explicit propagation schedules suggests it could generalize to other finite-dimensional geometric realizability questions, provided those questions admit a similarly rigid WLOG normalization.
The documented gap between the published count of 41 and the recomputed 43 final candidates implies that future reproductions of the bound must fix a canonical filter semantics before comparing candidate counts.
If the checker's soundness theorem is robust, the same certificate-and-replay architecture could be reused to certify non-embeddability in other orthogonality-graph problems, not just Kochen-Specker systems.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Quick take: this paper does the real work it claims. It replaces an uncheckable Z3 trust link in the geometric half of the Kochen–Specker lower bound with exact rational certificates, replayed by two independent checkers, and it proves soundness in Lean with per-graph verdicts as closed kernel theorems. It also surfaces genuine discrepancies in the published pipeline — injectivity as a load-bearing condition, a hidden WLOG branch, and an unreproducible candidate count. Those findings alone make it worth a close read.

The most solid part is the architecture. The certificate format is precise: WLOG anchoring, propagation schedules, factorization/SOS splits, and leaves discharged by injectivity, ideal membership, or a Positivstellensatz-style positivity argument. Every check is exact rational arithmetic. The soundness theorem covers all eight node kinds, and the non-embeddability results are stated as closed Lean theorems proved by decide. As far as I can tell from the PDF, the formal core holds up.

The soft spot is exactly where the stress-test note points: the bridge from the published blocking files to the graph objects the certificates live on. The certificates prove non-embeddability for embedded edge lists; the claim that these are the graphs from the published pipeline depends on a Python replay script and SHA-256 pins, not on a machine-checked theorem. The paper's own Findings 4 and 5 show the published files are subtle — missing trailing newline, 155 distinct versus 266 lines, 41 vs 43 candidates — so a parser bug would silently change the certified graph. That is a genuine artifact-trust gap. It could be closed by making the parser/serialization formally verified, or at least by providing a precise, machine-checked correspondence between source files and certificate graphs. This doesn't undermine the internal soundness of the Lean proofs, but it does constrain what you can conclude about the published bound.

I could not run the repository from the PDF. The claims about kernel reducibility and the 115-mutation adversarial suite are asserted from the repo, not demonstrated in the text. The two unresolved final candidates are handled honestly as explicit obligations, and the absence of an end-to-end ≥24 theorem is stated plainly. These are limitations, not red flags.

Who this is for: anyone working on verified computational proofs, and anyone who wants to know whether the geometric half of the KS bound is actually checked. It deserves a serious referee, with particular attention to the artifact and the parser bridge.

Referee Report

2 major / 5 minor

Summary. The paper introduces exact rational case-tree certificates for real non-embeddability of orthogonality graphs, and claims to certify all 291 source lines (180 distinct graphs) of the published PhysicsCheck blocking lists plus seven order-13 Uijlen–Westerbaan minimal graphs. The certificates are replayed by a pure-Python checker and by a total checker implemented in Lean 4, with a kernel-checked soundness theorem whose axiom closure is {propext, Classical.choice, Quot.sound}. Each per-graph non-embeddability result is claimed to be a closed kernel theorem proved by `decide`. The paper also reports findings about the published pipeline, including a load-bearing injectivity condition, hidden WLOG case obligations, and an unreproducible final-candidate count.

Significance. If the claims hold, this is a substantial contribution. It replaces an uncheckable Z3 nonlinear-real-arithmetic component of a flagship computational bound with exact, replayable certificates, and it does so with a machine-checked soundness theorem, a minimal and mechanically enforced axiom closure, kernel-reducible verdicts, and adversarial validation. The explicit treatment of unresolved obligations and the detailed audit of the published pipeline are also strengths. The main residual risk is the unformalized bridge from the published artifact files to the edge lists embedded in the certificates; this is an artifact-trust concern rather than an internal inconsistency, but it is load-bearing for the paper's central claim that the geometric half of the published bound is closed for the blocking database.

major comments (2)

[§5.1, Findings 4 and 5; §4.2] The central external claim — that the 291 source lines of the published blocking database are faithfully represented by the certificate edge lists — is not machine-checked. The only bridge is a Python replay script and SHA-256 pins, both outside the Lean kernel. The paper itself demonstrates that line counts and filter semantics are delicate (missing trailing newline, 155 vs 266 distinct lines, 41 vs 43 candidate counts). A parser or line-splitting error would make the closed kernel theorems correct but for the wrong graphs, so the claim that the geometric half of the published bound is closed would not transfer. Please provide the parsed edge lists for all 180 graphs as a standalone machine-readable artifact with an independent audit path, or formalize the parsing/provenance layer, and state the trust boundary explicitly in the abstract and introduction.
[§5.1, Finding 5] The statement that 42 of the 44 final order-22/23 candidates are discharged by seven order-13 certificates depends on the external 933-graph Uijlen–Westerbaan list and on a replication of the published filter whose semantics are not machine-checked. The paper's resolution of the 41/43 discrepancy is based on pinned artifacts, not on a Lean-verified classification. This is load-bearing for the claim that the order-13 row "does real work for the full bound." Please separate the machine-checked part (seven order-13 graphs are certified non-embeddable) from the external classification and containment analysis, or supply verified containment witnesses for the 42 candidates.

minor comments (5)

[§5.1] Please clarify the arithmetic relating "exactly 42 of the 44 contain one of seven order-13 UW minimal graphs" to Finding 5's statement that "exactly 41 contain an order-13 UW minimal graph" among the 43 order-23 survivors. The order-22 survivor must be accounted for explicitly.
[§3.3, Eq. (1)] In the `positiv` leaf, state explicitly that p_1,...,p_m are the residual pool polynomials of the current branch; the current text leaves this implicit.
[§4.2] The displayed theorem `c10_0_nonembeddable` refers to "graph #0" without showing the edge list. Either include the explicit colex edge list in the statement or provide a pointer to the pinned transcription so the reader can see what graph is being certified.
[Table 3] The row "order-12 shard 20" should clarify what a "shard" is and why only 20 certificates appear there while Table 2 lists 155 distinct order-12 graphs. The relationship between shards, source lines, and distinct graphs is not immediately clear.
[§2.2, Table 1] Consider stating explicitly that "closed for blocking DB" in the T5 row means the Z3 verdicts for the blocking database are replaced by certificates, not that the full T5 layer for all order-22/23 candidates is closed. Section 7 already scopes this, but Table 1 could be read too strongly.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the Lean kernel soundness theorem is proved against a semantic realization definition; certificates are independently replayed; per-graph data come from external published artifacts with provenance pins.

full rationale

Walking the derivation chain, the central claim is theorem check_sound (Section 4.1, Figure 2): if the total reflective checker Cert.check accepts a certificate, then no Realization (Definition 3.1) of that certificate's graph exists. This is kernel-checked under the minimal axiom closure {propext, Classical.choice, Quot.sound}, with no custom axioms and no native reduction. The per-graph theorem (e.g., c10_0_nonembeddable) is then obtained by kernel-reducible decide, so the soundness of the checker is not an input to any certificate; it is a general theorem over all certificates. The certificate graphs are bound to external published sources (PhysicsCheck order-10/11/12 blocking files and the Uijlen-Westerbaan order-13 minimal graphs) via pinned artifact hashes and a Python replay, not derived from or fitted to the checker's own verdicts. No certificate parameter is fitted to make acceptance true; no leaf discharges by appealing to the graph's membership in the published database. The paper explicitly scopes its result to the blocking database and does not claim a fully composed end-to-end bound: two final order-23 candidates are left as explicit machine-readable unresolved obligations, so nothing is being renamed as closure. The cited prior work is external and is used as data/artifacts, not as a self-citation chain. The residual risks identified in the paper — transcription fidelity between published source lines and embedded edge lists, exact filter semantics, and artifact provenance — are external trust concerns about the input data, not circular reductions. Findings 1-5 refine the understanding of the published pipeline but do not define the target conclusion in terms of the certificates. This is a normal, healthy formalization result: the soundness proof is self-contained, and the data provenance is separable from the verified derivation.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The central claim rests on Lean kernel axioms, standard real-geometry facts, and external data provenance. There are no fitted free parameters and no invented physical or mathematical entities: the certificate format and KRat arithmetic are proof infrastructure, not new postulated objects.

assumptions (4)

standard math Lean kernel axiom closure {propext, Classical.choice, Quot.sound}
Section 4.1: build-time axiom gate restricts to these three standard axioms; the soundness theorem is sorry-free and kernel-checked.
standard math Real-geometry lemmas: O(3) transitivity on anchored triads/edges, orthocomplement lemma, cross-product injectivity on distinct rays, plane-basis spanning, SOS-zero over formally real fields, factor-zero in integral domains
Section 4.1: seven lemmas consumed by the tree walk are proved in the development and are standard facts; listed as background rather than assumed ad hoc.
domain assumption Published artifact data provenance: extracted blocking lists, Uijlen-Westerbaan list, and candidate counts faithfully represent PhysicsCheck
Section 5.1 Findings 4-5: certificates bind to graph edge lists via #guard and Python replay against pinned SHA-256 artifacts; the kernel cannot prove this external correspondence.
domain assumption PhysicsCheck embeddability notion includes pairwise ray-distinctness for all vertex pairs
Finding 1: the Z3 encoding asserts cross(v_j,v_i)≠0 for all i≠j; the certified non-embeddability definition aligns with this, and the lower-bound transfer depends on this reading.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound." pith.science (2026). https://pith.science/paper/TXOULYRV

@misc{pith2026260726413,
  author       = {Pith},
  title        = {Pith review of: Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/TXOULYRV}},
  note         = {Machine review of arXiv:2607.26413}
}

abstract

The best known lower bound for the minimum Kochen-Specker vector system in $\mathbb{R}^3$ -- 24 vectors -- rests on a computational proof whose combinatorial half emits DRAT proofs but whose geometric half does not: the non-embeddability of thousands of candidate graphs is established by Z3's nonlinear real arithmetic, which produces no checkable proof objects. We close this gap for the proof's blocking database. We introduce exact rational case-tree certificates of real non-embeddability, whose splits are polynomial factorizations and rational sum-of-squares decompositions and whose leaves are discharged by injectivity, ideal-membership, or Positivstellensatz-shaped positivity arguments, and we certify all 291 source lines (180 distinct graphs) of the published pipeline's order-10 to order-13 blocking lists. Certificates are replayed by two independent checkers that share no code with the generator: a pure-Python replay over exact fractions, and a total checker implemented and proved sound in Lean 4. The soundness theorem -- acceptance implies that no injective-on-rays, orthogonality-respecting assignment of nonzero real vectors realizes the graph -- is kernel-checked with axiom closure {propext, Classical.choice, Quot.sound}, and a gcd-free rational arithmetic layer makes the entire verdict computation kernel-reducible, so each per-graph non-embeddability result is a closed kernel theorem proved by decide. The formalization surfaced findings about the published pipeline, including a load-bearing injectivity side condition in its embeddability notion, hidden WLOG case obligations invisible to Z3-based workflows, and an unreproducible candidate count that we resolve against the published artifacts. All certificates, checkers, and proofs are available and replayable from a single build.

Figures

Figures reproduced from arXiv: 2607.26413 by the authors.

**Figure 2.** The verified statement. check_sound is sorry-free with axiom closure {propext, Classical.choice, Quot.sound}. 3.5 Schema and normative deserialization Certificates ship as JSON (schema_version = 1) with fully structured polynomials: a monomial is a rational coefficient with positive denominator and a duplicate-free, exponent-positive variable list. Well-formedness is normative and enforced at ingestion by both chec… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

15 extracted references · 2 linked inside Pith

[1]

Felix Arends, Joël Ouaknine, and Charles W. Wampler. On searching for small Kochen–Specker vector systems.Graph-Theoretic Concepts in Computer Science (WG), pages 23–34, 2011

2011
[2]

Conway and Simon Kochen

John H. Conway and Simon Kochen. A 31-vector Kochen–Specker system, 1993. Reported in A. Peres,Quantum Theory: Concepts and Methods, Kluwer, 1993

1993
[3]

Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt, Matt Kaufmann, and Peter Schneider- Kamp. Efficient certified RAT verification. InAutomated Deduction (CADE), volume 10395 of LNCS, pages 220–236, 2017. 11

2017
[4]

Z3: An efficient SMT solver

Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. InTools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4963 of LNCS, pages 337–340, 2008

2008
[5]

The Lean 4 theorem prover and programming language

Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. InAutomated Deduction (CADE), volume 12699 of LNCS, pages 625–635, 2021

2021
[6]

InProceedings of the AAAI Conference on Artificial Intelligence, 2021

StephanGochtandJakobNordström.Certifyingparityreasoningefficientlyusingpseudo-Boolean proofs. InProceedings of the AAAI Conference on Artificial Intelligence, 2021. VeriPB proof system; dominance-based proof logging

2021
[7]

A Lean 4 formalization of the Kochen–Specker paradox.https://github.com/ guptbot/free_will_lean, 2025

Anand Gupta. A Lean 4 formalization of the Kochen–Specker paradox.https://github.com/ guptbot/free_will_lean, 2025

2025
[8]

Co-Certificate learning with SAT modulo symmetries

Markus Kirchweger, Tomáš Peitl, and Stefan Szeider. Co-Certificate learning with SAT modulo symmetries. InProceedings of the 32nd International Joint Conference on Artificial Intelligence (IJCAI), 2023

2023

Show all 15 references

[9]

Simon Kochen and Ernst P. Specker. The problem of hidden variables in quantum mechanics. Journal of Mathematics and Mechanics, 17(1):59–87, 1967

1967
[10]

Andrew Krapivin, Benjamin Przybocki, and Marijn J. H. Heule. Toward satisfiability modulo realizability. arXiv preprint, arXiv:2607.02958, 2026. To appear inCICM, 2026

2026 arXiv
[11]

Efficient verified (UN)SAT certificate checking.Journal of Automated Reasoning, volume 64, pages 513–532, 2020

Peter Lammich. Efficient verified (UN)SAT certificate checking.Journal of Automated Reasoning, volume 64, pages 513–532, 2020

2020
[12]

A SAT solver and computer algebra attack on the minimum Kochen–Specker problem

Zhengyu Li, Curtis Bright, and Vijay Ganesh. A SAT solver and computer algebra attack on the minimum Kochen–Specker problem. arXiv preprint, arXiv:2306.13319, 2024. Artifact repository: github.com/BrianLi009/PhysicsCheck

2024 arXiv
[13]

PBLean: Pseudo-Boolean proof certificates for Lean 4

Stefan Szeider. PBLean: Pseudo-Boolean proof certificates for Lean 4. arXiv preprint, arXiv:2602.08692, 2026

2026
[14]

A Kochen–Specker system has at least 22 vectors.New Gen- eration Computing, 34:3–23, 2016

Sander Uijlen and Bas Westerbaan. A Kochen–Specker system has at least 22 vectors.New Gen- eration Computing, 34:3–23, 2016

2016
[15]

Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. InTheory and Applications of Satisfiability Testing (SAT), volume 8561 of LNCS, pages 422–429, 2014. 12

2014

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.

[1] [1]

Felix Arends, Joël Ouaknine, and Charles W. Wampler. On searching for small Kochen–Specker vector systems.Graph-Theoretic Concepts in Computer Science (WG), pages 23–34, 2011

2011

[2] [2]

Conway and Simon Kochen

John H. Conway and Simon Kochen. A 31-vector Kochen–Specker system, 1993. Reported in A. Peres,Quantum Theory: Concepts and Methods, Kluwer, 1993

1993

[3] [3]

Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt, Matt Kaufmann, and Peter Schneider- Kamp. Efficient certified RAT verification. InAutomated Deduction (CADE), volume 10395 of LNCS, pages 220–236, 2017. 11

2017

[4] [4]

Z3: An efficient SMT solver

Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. InTools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4963 of LNCS, pages 337–340, 2008

2008

[5] [5]

The Lean 4 theorem prover and programming language

Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. InAutomated Deduction (CADE), volume 12699 of LNCS, pages 625–635, 2021

2021

[6] [6]

InProceedings of the AAAI Conference on Artificial Intelligence, 2021

StephanGochtandJakobNordström.Certifyingparityreasoningefficientlyusingpseudo-Boolean proofs. InProceedings of the AAAI Conference on Artificial Intelligence, 2021. VeriPB proof system; dominance-based proof logging

2021

[7] [7]

A Lean 4 formalization of the Kochen–Specker paradox.https://github.com/ guptbot/free_will_lean, 2025

Anand Gupta. A Lean 4 formalization of the Kochen–Specker paradox.https://github.com/ guptbot/free_will_lean, 2025

2025

[8] [8]

Co-Certificate learning with SAT modulo symmetries

Markus Kirchweger, Tomáš Peitl, and Stefan Szeider. Co-Certificate learning with SAT modulo symmetries. InProceedings of the 32nd International Joint Conference on Artificial Intelligence (IJCAI), 2023

2023