Formalization Roadmap

A useful quantum formalization grows through reusable mathematical interfaces. Begin with a small theorem whose statement is already clear, then build the structures needed by a larger class of results. The route below describes dependencies and candidate projects. It is not a claim that these projects have been completed in a particular proof assistant, nor a timetable for the entire subject.

Helpful background. Proof Assistant Preview explains how to inspect a checked theorem and its dependencies; Why Formalize Quantum Mechanics? explains why interface design matters.

Stage one: finite states and exact linear algebra

Choose a complex finite-dimensional space with an explicit orthonormal coordinate interface. Build normalized vectors, rank-one projectors, positive trace-one states, effects, and finite POVMs. A first project can show that a normalized vector produces a density operator and that the Born probabilities of a finite POVM sum to one.

The important output is a reusable theorem with the hypotheses exposed: the input space is nontrivial, the inner product convention is fixed, and positivity means a nonnegative quadratic form. A few matrix calculations are useful diagnostics, but the formal statement should quantify over its declared input family. Use Finite-Dimensional QM Formalization to keep coordinate and abstract definitions connected.

Next add explicit factor labels, tensor associators, swaps, and partial trace. Check a product-state marginal before attempting a protocol whose subsystems can be confused. Equal matrix dimensions alone do not certify that the correct register is retained.

Stage two: channels and compositional protocol statements

Define completely positive trace-preserving maps, instruments, and subnormalized branches. Construct channels from suitable Kraus families and prove closure under composition and tensor products. These interfaces support a first protocol theorem without rebuilding positivity arguments at every step.

A useful milestone is a parameterized channel identity on all input operators, followed by its extension with an untouched reference system. For measured protocols, state whether classical outcomes are retained, discarded, or postselected. For coherent circuit rewrites, specify whether equality is exact or only up to global phase. The quantum-information formalization guide shows why that choice matters under controlled use.

Approximate correctness is a separate milestone. Introduce an error metric and prove how errors compose before attaching numerical tolerances to a general circuit theorem.

Stage three: bounded Hilbert-space analysis

Move from finite matrices to complete Hilbert spaces and bounded operators. Establish the chosen adjoint, tensor completion, operator topologies, and trace-ideal interfaces. Finite-rank approximation can then be used through proved convergence results rather than an informal limit of arrays.

A candidate project is a theorem about partial trace on trace-class operators, with positivity, normalization, and trace-norm continuity specified. This stage already requires substantially more analysis than its finite counterpart. The Hilbert-space challenges identify quotient representatives, completeness, and topology issues that cannot be postponed indefinitely.

One can also pursue compact self-adjoint spectral theory at this level. Keep compactness in the theorem statement; a discrete eigenvector expansion does not cover a general continuous-spectrum Hamiltonian.

Stage four: measures, domains, and dynamics

A general self-adjoint spectral theorem needs projection measures, appropriate integration, and measurable functional-calculus domains. Partially defined operators require graph closure, dense-domain adjoints, and a meaningful operator-equality relation. The spectral formalization guide details these dependencies.

A natural dynamics milestone connects a self-adjoint operator to its strongly continuous unitary group and distinguishes strong solutions on the operator domain from mild evolution on the whole Hilbert space. Time-dependent domains, singular perturbations, and unbounded open-system generators should be separate projects with their own hypotheses, not unchecked corollaries of the time-independent theorem.

Stage five: a model whose analytic boundary is explicit

Choose a model that exercises the established interfaces. Interval momentum tests boundary conditions and domain equality. A harmonic oscillator tests a complete eigenbasis and an unbounded graph domain. A point interaction tests a singular model defined through matching conditions or forms. The rigorous models chapter supplies the corresponding mathematical statements.

A completed model project should identify the exact operator realization, the theorem proved about it, and which physical approximation relates it to an experiment. A formal proof of one realization does not choose the boundary condition on behalf of the physical problem.

Across every stage, preserve an ordinary mathematical statement, the formal declaration, dependency assumptions, and a reproducible source/version record. A good stopping point is a useful theorem with a clear interface, not an impressive file count or an unqualified claim that “quantum mechanics is verified.”

Exercise: choose the dependency that cannot be skipped

A project has finite-dimensional diagonalization and wants to prove unitary time evolution for the free particle on the line. Why is taking larger finite matrices alone insufficient? Name two additional obligations.

Solution

The free Hamiltonian is an unbounded operator on an infinite-dimensional space and has continuous spectrum. One must specify and prove the self-adjoint realization, including its domain, and construct the relevant spectral calculus or unitary group. If finite matrices are used as approximants, one also needs a convergence theorem in a stated topology that relates their dynamics to that realization. Finite diagonalization alone supplies none of these analytic identifications.

References

• Hall, Brian C., Quantum Theory for Mathematicians, Graduate Texts in Mathematics 267, Springer, 2013, doi:10.1007/978-1-4614-7116-5 — the mathematical progression from finite systems to unbounded operators.
• Lean Project, Theorem Proving in Lean 4, official text — definitions, theorem interfaces, and proof construction.
• Watrous, John, The Theory of Quantum Information, Cambridge University Press, 2018, doi:10.1017/9781316848142 — finite quantum structures and compositional information-theoretic statements.