{"id":"arxiv/2604.03884","url":"https://arxiv.org/abs/2604.03884","tags":["quant-ph","cs.LO"],"score":0,"title":"Formalizing CHSH Rigidity in Lean 4","domain":"quant-ph","source":"arxiv","authors":["Tianrun Zhao","Nengkun Yu"],"reviews":0,"subject":"quant-ph","summary":"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).","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"discussed":0,"published":"2026-04-04","reactions":{}}