Formalization and Verification

Formalization makes a mathematical statement and its derivation explicit enough for mechanical checking. Quantum mechanics gives it demanding interfaces: positivity, tensor factors, partial operator domains, spectral measures, and several notions of convergence. This chapter explains how to read and design those interfaces, and how to state exactly what a computational or formal artifact has established.

The pages provide mathematical guidance and a reproducible exact-matrix example. They do not assert that the entire volume has been translated into a proof assistant. Published formal developments are used as concrete examples of methods, with their own stated scope.

Enter the chapter

Begin with Why Formalize Quantum Mechanics? for motivation and examples of hidden assumptions. Continue to Formal Proofs versus Human Proofs to separate three questions: whether the statement matches the intended problem, whether the derivation is valid, and whether the mathematical model describes a physical system.

Proof Assistant Preview then explains theorem types, proof states, dependency assumptions, and reproducible checking. Read it before interpreting an editor’s success indicator as a proof of the intended quantum claim. A checked implication may still rely on a hypothesis that the application has not established.

Start with finite quantum structures

Finite-Dimensional QM Formalization organizes states, effects, channels, and tensor factors into reusable interfaces. It explains why a positive matrix is not a matrix with positive entries, why a branch differs from a deterministic channel, and why equal array sizes do not identify the correct subsystem.

Quantum Information Theorems in Proof Assistants moves from isolated matrices to programs and protocols. Its central question is whether the chosen equivalence survives the intended context. An overall phase can become observable under coherent control; a protocol must preserve reference correlations when it claims channel identity; and terminating branches do not by themselves establish total correctness.

These pages assume familiarity with density operators and quantum operations. The canonical physics derivations remain linked at the point their mathematical statements are used.

Keep the infinite-dimensional transition explicit

Hilbert Space Formalization Challenges addresses completeness, almost-everywhere quotient vectors, partial operators, adjoints, graph norms, and completed tensor products. A formula on smooth functions does not automatically define an operator on every Hilbert vector.

Spectral Theorem Formalization Challenges distinguishes finite diagonalization from compact, bounded, and unbounded spectral statements. It explains why a projection measure needs strong operator additivity and why a measurable functional calculus must return a domain as well as an action. A bounded transform can help organize a proof while leaving genuine endpoint and integrability obligations.

Read the operator chapter and spectral chapter alongside these formalization pages. A proof language makes the hypotheses visible; it does not remove the need to understand them.

Run a small exact example and interpret its result

Verified Examples contains a complete Python/SymPy script for a complex rank-one projector, a dephasing channel’s Choi matrix, and an exact negative witness for transposition’s failure of complete positivity. The checks use exact arithmetic and explicitly state the tensor and normalization conventions.

The example distinguishes a symbolic calculation from a proof-assistant kernel proof. It also includes a negative control: a check should reject the deliberately invalid complete-positivity claim, not merely accept well-behaved examples. A reproduction records versions and the unchanged source so the same assertions can be inspected and rerun.

Choose a project with a mathematical stopping point

Formalization Roadmap gives a dependency-based sequence from finite states to channels, bounded Hilbert-space analysis, spectral measures, and selected unbounded models. Each stage suggests a useful theorem interface and identifies what would remain to be proved before moving further.

The goal of a first project is a clear, reusable result with a reproducible proof and understood assumptions. A small exact theorem can be more valuable than a broad claim whose definitions, admitted dependencies, or physical interpretation cannot be inspected.

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 operator framework.
• Lean Project, Theorem Proving in Lean 4, official text — formal statements and proof construction.
• Nipkow, Tobias, Programming and Proving in Isabelle/HOL, tutorial, 18 January 2026 edition, official PDF — structured formal proofs.
• Watrous, John, The Theory of Quantum Information, Cambridge University Press, 2018, doi:10.1017/9781316848142 — the state, channel, and protocol mathematics used by the examples.