arxiv: 2604.03884 · v1 · submitted 2026-04-04 · 🪐 quant-ph · cs.LO

Recognition: 2 theorem links

· Lean Theorem

Formalizing CHSH Rigidity in Lean 4

Tianrun Zhao , Nengkun Yu

Authors on Pith no claims yet

Pith reviewed 2026-05-13 16:42 UTC · model grok-4.3

classification 🪐 quant-ph cs.LO

keywords CHSH inequalityrigidity theoremquantum strategiesLean 4formal verificationself-testingBell inequalities

0 comments

The pith

A Lean 4 formalization establishes that any strategy achieving near-optimal CHSH value must be locally isometric to the canonical qubit strategy.

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

This paper formalizes the CHSH rigidity theorem inside the Lean 4 theorem prover. The theorem states that any quantum strategy whose CHSH value comes close to the Tsirelson bound must be equivalent, via local isometries, to the standard strategy in which two parties share a Bell state and measure in complementary bases. In carrying out the formalization the authors locate and repair an incompleteness in the 2012 argument of McKague, Yang and Scarani. A sympathetic reader cares because the result supplies a machine-checked guarantee that high CHSH violation can be used as reliable evidence of the standard entangled qubit resource.

Core claim

The central claim is that any quantum strategy attaining a CHSH value sufficiently close to the quantum maximum is locally isometric to the canonical strategy in which Alice and Bob share the two-qubit Bell state and perform the standard X and Z measurements; the Lean 4 script confirms this after correcting the identified gap in the earlier proof.

What carries the argument

The CHSH rigidity theorem, which extracts the local-isometry equivalence from the near-optimality of the CHSH value.

If this is right

Machine-checked rigidity supplies a verified foundation for device-independent certification that relies on CHSH violation.
The same formal approach can be reused for self-testing statements attached to other Bell inequalities.
Quantitative versions of the theorem become feasible once the proof script is available.
The repaired argument clarifies which steps in the 2012 reasoning were incomplete.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Computer-assisted proofs of this kind could be chained with formalizations of cryptographic protocols that rest on CHSH self-testing.
The gap fix may yield explicit bounds on how close a strategy must be to the ideal one before the isometry guarantee applies.
Similar formalizations of other rigidity results would strengthen the logical basis of device-independent quantum information.

Load-bearing premise

The Lean 4 encoding faithfully captures the definitions of quantum strategies, local isometries, and the CHSH value.

What would settle it

An explicit quantum strategy that reaches a CHSH value arbitrarily close to the Tsirelson bound yet cannot be turned into the standard Bell-pair strategy by any local isometries on Alice's and Bob's sides.

read the original abstract

Violation of the Clauser-Horne-Shimony-Holt (CHSH) inequality certifies genuine quantum correlations. In this work, we formalize in Lean 4 the rigidity theorem -- any strategy achieving near-optimal CHSH value must be locally isometric to the canonical qubit strategy. In the course of formalization, we identified a gap in the argument of McKague, Yang, and Scarani (arXiv:1203.2976).

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This Lean 4 formalization of CHSH rigidity confirms the local isometry claim with a machine-checked proof and flags a fixable gap in the 2012 McKague-Yang-Scarani argument.

read the letter

The main takeaway is a verified Lean 4 proof that any quantum strategy close to the optimal CHSH value is locally isometric to the standard qubit strategy, plus an explicit repair for a gap in the earlier McKague et al. paper. The formalization starts from standard definitions of quantum strategies, measurements, and the CHSH functional, then derives the rigidity statement inside Lean against existing math libraries. That approach removes the usual risk of overlooked cases in analytic arguments. The gap report is a practical side benefit; it shows where the 2012 informal proof skipped a step, but the formal version closes it without changing the final theorem. This kind of machine-checked work is genuinely useful when people later build device-independent protocols on top of rigidity results. The definitions are pinned down in code, so anyone can inspect or extend them directly. On the soft side, the paper is still a formalization of an established theorem rather than a new physical or mathematical claim. Its reach stays inside quantum foundations and formal methods. The abstract notes the gap but does not spell out the repair in detail, so readers may need to look at the Lean code itself to see exactly how the missing piece was handled. No free parameters or invented entities appear, and the proof avoids circularity by building from external libraries. This is the sort of paper that matters for groups doing verified quantum information or anyone who needs a reliable reference for CHSH-based self-testing. A serious editor should send it to peer review because the machine-checked proof supplies concrete evidence of soundness and the gap identification adds a usable correction to the literature.

Referee Report

0 major / 2 minor

Summary. The manuscript formalizes in Lean 4 the CHSH rigidity theorem: any quantum strategy achieving a CHSH value sufficiently close to the Tsirelson bound 2√2 must be locally isometric to the canonical two-qubit strategy. In the course of the formalization the authors identify and repair a gap in the 2012 argument of McKague, Yang and Scarani.

Significance. If the formalization is faithful, the work supplies a machine-checked, parameter-free derivation of a central self-testing result in quantum information. This strengthens the foundations for device-independent protocols by eliminating unverified analytic steps and providing an explicit, reproducible proof against standard mathematical libraries.

minor comments (2)

[Abstract] Abstract: the precise location of the gap in McKague et al. (arXiv:1203.2976) is not indicated; adding a reference to the affected lemma would help readers locate the repair.
[§3.2] §3.2: the Lean definition of the local isometry could be accompanied by a short inline mathematical expression to ease comparison with the informal statement.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary, recognition of the significance of the machine-checked proof, and recommendation to accept the manuscript. No major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper delivers a machine-checked Lean 4 formalization of the CHSH rigidity theorem, proceeding directly from explicit, standard definitions of quantum strategies, isometries, and the CHSH value that are verified by the Lean kernel against external mathematical libraries. No derivation step reduces by construction to a fitted parameter, self-definition, or load-bearing self-citation; the gap noted in the 2012 McKague-Yang-Scarani paper (non-overlapping authors) is repaired inside the formal development itself rather than imported as an unverified premise. The central claim therefore remains independent of the paper's own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work is a formalization of existing mathematics; no new free parameters, ad-hoc axioms, or invented entities are introduced.

axioms (1)

standard math Standard axioms of quantum mechanics, Hilbert spaces, and linear algebra as provided by Lean's mathlib
The formalization relies on these background libraries for all definitions of states, measurements, and isometries.

pith-pipeline@v0.9.0 · 5356 in / 1109 out tokens · 72678 ms · 2026-05-13T16:42:39.422953+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

13 extracted references · 13 canonical work pages · 1 internal anchor

[1]

Quantum generalizations of bell’s inequality

Boris S Cirel’son. Quantum generalizations of bell’s inequality. Letters in Mathematical Physics, 4(2):93–100, 1980

work page 1980
[2]

Proposed experiment to test local hidden-variable theories

John F Clauser, Michael A Horne, Abner Shimony, and Richard A Holt. Proposed experiment to test local hidden-variable theories. Physical review letters , 23(15):880, 1969

work page 1969
[3]

Qic 890 entanglement and nonlocal effects, April 2019

Richard Cleve. Qic 890 entanglement and nonlocal effects, April 2019. URL https://cleve. iqc.uwaterloo.ca/resources/Qic890LectureNotes2019Apr22(V22).pdf. Lecture notes for QIC 890, University of Waterloo

work page 2019
[4]

Consequences and lim- its of nonlocal strategies

Richard Cleve, Peter Hoyer, Benjamin Toner, and John Watrous. Consequences and lim- its of nonlocal strategies. In Proceedings. 19th IEEE Annual Conference on Computational Complexity, 2004. , pages 236–249. IEEE, 2004

work page 2004
[5]

Top 100 quantum theorems, 2026

Marco David and Jens Palsberg. Top 100 quantum theorems, 2026. URL https://marcodavid. net/top100/. Accessed 2026-03-26

work page 2026
[6]

The lean theorem prover (system description)

Leonardo De Moura, Soonho Kong, Jeremy A vigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In International Conference on Automated Deduction, pages 378–388. Springer, 2015

work page 2015
[7]

Artur K. Ekert. Quantum cryptography based on bell’s theorem. Phys. Rev. Lett. , 67:661– 663, Aug 1991. doi: 10.1103/PhysRevLett.67.661. URL https://link.aps.org/doi/10.1103/ PhysRevLett.67.661

work page doi:10.1103/physrevlett.67.661 1991
[8]

Self testing quantum apparatus

Dominic Mayers and Andrew Yao. Self testing quantum apparatus. arXiv preprint quant- ph/0307205, 2003

work page arXiv 2003
[9]

Robust self-testing of the singlet

M McKague, T H Yang, and V Scarani. Robust self-testing of the singlet. Journal of Physics A: Mathematical and Theoretical , 45(45):455304, oct 2012. doi: 10.1088/1751-8113/45/45/ 455304. URL https://doi.org/10.1088/1751-8113/45/45/455304

work page doi:10.1088/1751-8113/45/45/ 2012
[10]

Lessa, and Rodolfo R

Alex Meiburg, Leonardo A. Lessa, and Rodolfo R. Soldati. A formalization of the generalized quantum stein’s lemma in lean, 2025. URL https://arxiv.org/abs/2510.08672

work page arXiv 2025
[11]

CoRRabs/2602.08734(2026)

Yuanjie Ren, Jinzheng Li, and Yidi Qi. Merlean: An agentic framework for autoformalization in quantum computation. arXiv preprint arXiv:2602.16554 , 2026. doi: 10.48550/arXiv.2602. 16554

work page doi:10.48550/arxiv.2602 2026
[12]

The lean mathematical library

The mathlib Community. The Lean Mathematical Library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs , CPP 2020, New Orleans, LA, USA, January 2020. ACM. doi: 10.1145/3372885.3373824. URL https: //doi.org/10.1145/3372885.3373824

work page doi:10.1145/3372885.3373824 2020
[13]

Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature

Joseph Tooby-Smith. Formalizing the stability of the two higgs doublet model potential into lean: identifying an error in the literature, 2026. URL https://arxiv.org/abs/2603.08139. 11

work page internal anchor Pith review Pith/arXiv arXiv 2026