← All papers
Formalizing CHSH Rigidity in Lean 4
quant-ph
Apr 4, 2026 · v1
TL;DR
Formalizes the CHSH rigidity theorem in Lean 4 (and finds a gap in a prior proof).
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).
Problem
The CHSH inequality rigidity theorem states that any strategy achieving near-optimal CHSH value must be locally isometric to the canonical qubit strategy, but no formal machine-checked proof existed.
Approach
The authors formalize the CHSH rigidity theorem in Lean 4, proving that near-optimal CHSH strategies must be locally isometric to the canonical qubit strategy. During formalization, they identified a gap in the argument of McKague, Yang, and Scarani (arXiv:1203.2976).
Results
The rigidity theorem is fully formalized in Lean 4. The formalization uncovered a gap in a prior published proof by McKague, Yang, and Scarani.