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

• URL: http://arxiv.org/abs/2607.26413v1
• Date: Wed, 29 Jul 2026 02:53:00 GMT
• Title: Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound
• Abstract summary: The best known lower bound for the minimum Kochen-Specker vector system in $mathbbR3$ rests on a computational proof whose half emits DRAT but whose geometric half does not.<n>We introduce exact rational case-tree certificates of real nonembeddability, whose splits are factorizations and rational sum-of-squares decompositions.<n>All certificates, checkers, and proofs are available and replayable from a single build.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• AutoGraphForge: Towards Automated Graph Theory Discovery [0.0]
  AutoGraphForge is an automated graph-theoretic conjecturing-refuting-formalizing-trivial system.<n>A novelty filter decides via a linear program whether a candidate is already implied by known results.<n>Run for several rounds on an HPC cluster, the loop yields $6,522$ conjectures that survived the refutation dataset.
  arXiv  Detail & Related papers  (2026-09-03T07:35:29Z)
• ProofPulse: Interactive Proof Coverage Analysis for Dafny [47.23158426199152]
  Deductive verification ensures that an implementation satisfies its specification, but successful verification does not guarantee the quality of the specification.<n>We present proofpulse, a tool for Dafny that diagnoses specification quality using a three-valued proof coverage model.
  arXiv  Detail & Related papers  (2026-08-31T14:00:31Z)
• Formalizing Flag Algebras in Lean [8.924529562496874]
  Razborov's flag algebra method is a powerful tool for proving inequalities in extremal graph theory.<n>We present a machine-checked formalization of the method, together with a certificate-to-proof compiler.<n>Case studies yield formal proofs of seven Turn-type upper bounds.
  arXiv  Detail & Related papers  (2026-07-26T07:07:29Z)
• Byzantine Accountability Without Consensus: Strong Eventual Consistency for Non-Associative, Stochastic, Robust Aggregation [0.0]
  ACFA replicates a content-addressed OR-Set of signed contributions and a grow-only set of self-authenticating equivocation proofs.<n>A prototype (10 nodes, 3 Byzantine) passes 16/16 falsification checks.
  arXiv  Detail & Related papers  (2026-07-11T13:23:06Z)
• Harnessing Code Agents for Automatic Software Verification [0.47154736035631406]
  Large language models (LLMs) promise to generate proofs automatically, yet existing approaches wire a fixed, human-designed proof strategy into the system.<n>We show that imposing such a strategy is unnecessary and limiting.<n>Handing the whole lemma to a general code agent, free to choose its own approach, and wrapping it in a verification harness is both simpler and more effective.
  arXiv  Detail & Related papers  (2026-07-07T14:39:59Z)
• ZX-Calculus:Trace-Indexed Dependent Types and Epistemic Semantics [3.848983210046659]
  We propose ZX-Calculus (Knowledge Evolution Calculus), a conservative extension of Martin-Lof Dependent Type (MLTT)<n>It integrates trace-indexed types, presheaf non-monotone semantics, and constructive AGM belief revision.<n>A Coq mechanisation accompanies the paper (34 complete proofs; zero admits for the two central results)
  arXiv  Detail & Related papers  (2026-06-02T02:51:41Z)
• Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
  We present a formally verified framework for patent analysis as a hybrid AI + Lean 4 pipeline.<n>The DAG-coverage core (Algorithm 1b) is fully machine-verified once bounded match scores are fixed.<n>Claims are encoded as DAGs in Lean 4, match strengths as elements of a verified complete lattice, and confidence scores propagate through dependencies via proven-correct monotone functions.
  arXiv  Detail & Related papers  (2026-04-20T22:02:57Z)
• Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1 [51.56484100374058]
  System extracts tactic usage distributions across 27 top-level areas of Mathlib.<n>It computes z-scores to identify tactics that are heavily used in a source area but rare or absent in a target area.<n>It matches source and target proof states via GPU-accelerated NP-hard analogy.
  arXiv  Detail & Related papers  (2026-04-19T03:27:16Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  We present LiveMathematicianBench, a dynamic multiple-choice benchmark for research-level mathematical reasoning.<n>By grounding evaluation in newly published theorems, it provides a realistic testbed beyond memorized patterns.<n>It employs a proof-sketchguided distractor pipeline that uses high-level proof strategies to construct plausible but invalid answer choices.
  arXiv  Detail & Related papers  (2026-04-02T08:22:17Z)
• TorchLean: Formalizing Neural Networks in Lean [71.68907600404513]
  We introduce TorchLean, a framework that treats learned models as first-class mathematical objects with a single, precise semantics shared by execution and verification.<n>We validate TorchLean end-to-end on certified robustness, physics-informed residual bounds for PINNs, and Lyapunov-style neural controller verification.
  arXiv  Detail & Related papers  (2026-02-26T05:11:44Z)
• General Cutting Planes for Bound-Propagation-Based Neural Network Verification [144.7290035694459]
  We generalize the bound propagation procedure to allow the addition of arbitrary cutting plane constraints. We find that MIP solvers can generate high-quality cutting planes for strengthening bound-propagation-based verifiers. Our method is the first verifier that can completely solve the oval20 benchmark and verify twice as many instances on the oval21 benchmark.
  arXiv  Detail & Related papers  (2022-08-11T10:31:28Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  We present a novel stepwise method NLProofS (Natural Language Proof Search) NLProofS learns to generate relevant steps conditioning on the hypothesis. It achieves state-of-the-art performance on EntailmentBank and RuleTaker.
  arXiv  Detail & Related papers  (2022-05-25T02:22:30Z)
• Scalable Sampling for Nonsymmetric Determinantal Point Processes [47.18450267217498]
  A determinantal point process (DPP) on a collection of $M$ items is a model, parameterized by a symmetric kernel matrix. Recent work shows that removing the kernel symmetry constraint, yielding nonsymmetric DPPs (NDPPs), can lead to significant predictive performance gains for machine learning applications. There is only one known DPP sampling algorithm, based on Cholesky decomposition, that can directly apply to NDPPs as well. We show that imposing certain structural constraints on the NDPP kernel enables us to bound the rejection rate in a way that depends only on the kernel rank.
  arXiv  Detail & Related papers  (2022-01-20T19:21:59Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.