About Lean-QuantumInfo
Lean 4 formalization of quantum information theory. Covers quantum entropy, channels, and proved the Generalized Quantum Stein’s Lemma — the deepest mathematical result in any quantum verification project.
Scope and Goal
| Aspect | Lean-QuantumInfo | Fanal |
|---|---|---|
| Domain | Quantum information theory | Quantum programming language verification |
| Driving goal | Prove the Generalized Quantum Stein's Lemma (GQSL) | Verify quantum program correctness, culminating in Shor's algorithm |
| Nature of output | Proved mathematical theorems (no-cloning, trace distance, GQSL) | Typed DSL with denotational semantics, equational reasoning, and planned Hoare logic |
| Target audience | Quantum information theorists | Quantum PL researchers, formal methods community |
Mathematical Foundation
| Aspect | Lean-QuantumInfo | Fanal |
|---|---|---|
| Mathlib usage depth | Deep: PosSemidef, IsHermitian, ENNReal, Filter.Tendsto, topology | Selective: Matrix, conjTranspose, PosSemidef, Complex, Fintype |
| Analysis infrastructure | Extensive: limits, compactness, semicontinuity, extended nonneg reals | Not engaged; focuses on linear algebra and matrix semantics |
| Mathlib contributions | 10+ upstream PRs (eigenvalues, convex sets, trace lemmas) | None reported |
| Mathematical depth | Very deep: GQSL involves convergence of hypothesis testing rates | Applied: Dirac notation semantics, operator predicates, Loewner order |
Quantum State Representation
| Aspect | Lean-QuantumInfo | Fanal |
|---|---|---|
| Core type | MState d: Hermitian matrix + positivity + trace-one | DiracTerm AST: kets, bras, operators, scalars |
| Type safety | Lean wrapper types (HermitianMat, MState, Ket, Bra) prevent ill-typed operations | Custom typing relations (DiracWellTyped, LDiracWellTyped) |
| Semantics style | Direct mathematical definitions on structured types | Denotational: AST -> Option (Matrix ...) |
| Mixed states | First-class: MState bundles density matrix properties | Expressible via operator sort, but not a dedicated type |
Type System Approach
| Aspect | Lean-QuantumInfo | Fanal |
|---|---|---|
| Philosophy | Lean's native type system + wrapper structs | Custom embedded type system (DataType, DiracSort, UnifiedType) |
| Type checking | Lean's type checker is the type system | Explicit typing judgment as an inductive relation |
| Context | Lean's native context (implicit) | UnifiedContext: list of (Var, UnifiedType) bindings |
| Bridging | Would require explicit compilation from Fanal terms to QuantumInfo structures | Would require explicit compilation from Fanal terms to QuantumInfo structures |
Unique to Lean-QuantumInfo
| Aspect | Lean-QuantumInfo | Fanal |
|---|---|---|
| Entropy theory | Von Neumann entropy, quantum relative entropy, sandwiched Renyi relative entropy | Not in scope |
| Resource theories | FreeStateTheory, ResourceTheory, tensor product closure | Not in scope |
| GQSL | Largest single theorem in physics formalized in Lean | Not in scope |
| Trace distance | Formal definition and D(rho, sigma) <= 1 bound | Not formalized |
| Circuit verification tactic | matrix_expand for automated qubit gate reasoning | dirac_eq for Dirac notation equalities (different domain) |
Unique to Fanal
| Aspect | Lean-QuantumInfo | Fanal |
|---|---|---|
| Dirac notation DSL | Not available | Full AST with kets, bras, scalars, variadic operations, big sums/tensors |
| Hierarchical register labels | Not available | Access-path model for multi-register systems (tuple/array indexing) |
| Labelled Dirac notation | Not available | Register-annotated Dirac terms with disjointness premises |
| Classical expression language | Not available | CExprTerm with variables, arithmetic, booleans, arrays |
| Equational reasoning framework | Not available | SemEq, HSemEq, SortIso, DTIso for term equivalence across sorts |
| Planned program logic | Not in scope | Quantum Hoare logic, assertion language, program verification |
Maturity
| Aspect | Lean-QuantumInfo | Fanal |
|---|---|---|
| Theorems | 1,000+ proved theorems | Growing (supportive proofs + equational rules) |
| LOC | ~15,000 (as of Oct 2025 paper) | ~24,500 |
| Contributors | 3+ (Meiburg, Lessa, Soldati, Bailey, Wu) | 1 primary (Yingte Xu) + AI agents |
| Flagship result | Generalized Quantum Stein's Lemma | Dirac notation equational reasoning framework |
| Development model | Traditional human-driven | AI-augmented (Claude Code agents, Steward workflow) |
Potential Synergies
| Aspect | Lean-QuantumInfo | Fanal |
|---|---|---|
| Loewner order | Mature HermitianMat with Loewner order construction | Could import or align with QuantumInfo's ordering |
| Entropy & distance | Could provide entropy and trace distance for Fanal's assertion reasoning | Could use these for program specification properties |
| Dirac notation for QuantumInfo | Could benefit from Fanal's notation layer | Provides physicist-friendly notation |
| Register management | Could use Fanal's label system for multi-party scenarios | Provides systematic access-path approach |
Summary: Key Differences
| Aspect | Lean-QuantumInfo | Fanal |
|---|---|---|
| Proof System | Lean 4 / Mathlib | Lean 4 / Mathlib |
| Focus | Quantum information theory (entropy, channels) | Quantum program formalization & verification |
| Language | No programming language | Classical-quantum programming language |
| Math Depth | Very deep (Generalized Quantum Stein’s Lemma) | Applied (Dirac notation, Hoare logic) |
| Complementarity | Information-theoretic foundations | Program verification toolchain |