🚀 Announcing QECLean, our effort to formalize quantum error correction and fault-tolerance in Lean. The effort is led by PhD student, Stavan Jain.
We have a full formalization of the Toric Code and a proof of its distance, [[2L^2, 2, L]]! And more to come...