Lean for Science

Quantum mechanics with the proofs attached. Lean 4 theorems about quantum systems live inside Marimo reactive notebooks next to the SymPy computations they justify, so a result can be explored numerically and verified formally in one place. It is the working end of the Formal Verification in Science theme: the notebooks are where PhysLib's formalizations meet a course, an experiment or a digital twin.

Spin-½ structure, proved in Lean 4 against Mathlib:

• The Pauli matrices as explicit 2×2 complex matrices, and their squares
• The commutation relations among them
• The ladder operators built from them
• A no-go theorem: no finite set of n×n matrices satisfies the canonical commutation relation, because the trace of a commutator vanishes while the trace of the identity is n. Every truncated numerical Fock space is therefore an approximation, and the corner artifact a QuTiP simulation shows is unavoidable rather than a bug.
• Energy conservation in the Jaynes–Cummings model

Each claim is encoded twice, in Lean and in SymPy, and the two encodings are checked against each other. Matrix identities are reduced to a scalar that must evaluate to zero.

Lean 4 + Mathlib — the proofs, compiled locally with Lake or through the VVUQ verification service, with a soundness gate that rejects sorry, native_decide and added axioms.

Marimo + SymPy — a Lean InfoView panel shows goals, diagnostics and hover types as the code changes; a SymPy panel evaluates each line and shows the result beside it.

One bundle — the theorems compile together as a single module under the formalization-consistency standard, so a proof about a Pauli matrix and a proof about a Hamiltonian are provably about the same objects, not two definitions that never meet. The same Lean sources feed the notebook ladders and the documentgraph, by reference rather than by copy, so the two cannot drift.

GitHub repository — clone it and run marimo edit notebooks/angular_momentum_exercises.py, or open the course_angular_momentum, lean_infoview and QuTiP-lecture notebooks.

Related: the NV Diamond Lean Tutorial applies the same approach to quantum sensing, and VVUQ is the verification backend the notebooks compile against.