∀⚛️✅ Quantum information in Lean

Lean is both a functional programming language, and a highly extensible proof checker: originally intended more for checking proofs of correctness of code, it has been used to develop an expansive theory of math ("mathlib") with proofs of much standard mathematical curriculum. Our project tries to apply these theorems to physics as well, with a large particular emphasis on quantum information and quantum computing. We would love help proving some "classic" facts about quantum information!

AI assistance is also encouraged for writing the proofs, with some caveats; more details can be found on the repo.