Why Formalize Quantum Mechanics?

Formalizing quantum mechanics means expressing chosen mathematical definitions and arguments in a language whose inference rules can be checked mechanically. Its immediate value is precision and reuse: a domain hypothesis or tensor-factor convention becomes an explicit part of the theorem interface. It does not turn a mathematical model into an experimentally established law, and it does not replace an explanation of why a theorem matters.

Helpful background. What Counts as Rigorous? distinguishes complete arguments from proof sketches; Tracking Domains explains the assumptions most easily lost in operator notation.

A formal statement forces the input to be specified

Consider “every state vector determines a normalized rank-one projector.” The intended construction is

$$P_\psi=\frac{|\psi\rangle\langle\psi|}{\|\psi\|^2}.$$

It requires $\psi\ne0$. One can encode that requirement as a theorem hypothesis, use normalized vectors as the input type, or work directly with rays. These choices expose different interfaces but must describe the same physical object. Allowing the zero vector and assigning an arbitrary value to division by zero in a total formal language would not repair the physical statement. The desired theorem must still express the intended nonzero-state condition.

The same discipline becomes more consequential for an unbounded Hamiltonian. The notation $H\psi$ requires membership in $D(H)$, while $e^{-itH}\psi$ exists for every Hilbert vector when $H$ is self-adjoint. A formal interface should preserve that difference rather than silently assigning an arbitrary action outside the domain. The Schrödinger equation treatment distinguishes the corresponding strong and mild evolution statements.

Reusable interfaces can prevent repeated mistakes

A theorem about a channel should receive a channel together with its proofs of complete positivity and trace preservation. A theorem about a tensor product should identify the input and output factors, not rely on matching matrix sizes alone. Once these structures are established, later arguments can use their laws without reproving component calculations.

For example, composing two trace-preserving maps is a reusable theorem. An application to a particular noise model then only has to establish that the model satisfies the channel interface. This separation between a general interface and its concrete instances is one reason formalization can be more valuable than checking a long list of isolated formulas.

It also makes assumptions inspectable. Finite dimensionality, completeness, separability, or classical choice may enter at different steps. A dependency graph can reveal which later results genuinely require them. Such a graph is useful only when the definitions and imported statements have been read with the same care as the final proof.

Different checks answer different questions

A numerical calculation tests particular inputs up to numerical error. An exact symbolic calculation can certify a finite identity without rounding. A proof assistant checks a derivation in its formal foundation relative to its declared assumptions and trusted components. These methods answer complementary questions and should be named accurately.

An exact check that two specified matrices commute does not prove a theorem about every operator on a Hilbert space. Conversely, a formal theorem about an ideal circuit does not establish that a laboratory pulse sequence implements that circuit to a given fidelity. The map from physical device to mathematical model still requires physical justification.

Verified Examples illustrates exact finite calculations with explicitly limited claims. Formal Proofs versus Human Proofs explains how mathematical exposition and kernel checking contribute different parts of a convincing result.

Costs and limits belong in the motivation

Building a useful library requires choices about representations, coercions, tensor associativity, partial operators, and integration. Translating a textbook line can require substantial infrastructure. That effort is justified when the result is reusable or the hidden assumptions are important; formalization is not a guarantee of a short project.

A mechanically accepted theorem can still formalize the wrong claim, rely on an unwanted axiom, or concern an oversimplified model. The appropriate response is to inspect the statement and its dependencies, not to treat a successful tool run as a universal certificate. Official proof-assistant documentation explains these trust boundaries; the proof-assistant guide turns them into a concrete reading workflow.

Exercise: find the missing hypothesis

A proposed theorem says that every complex Hilbert space has a normalized vector. Identify a counterexample and state a corrected version. Why is this relevant to quantum formalization rather than merely a technicality?

Solution

The zero-dimensional Hilbert space contains only the zero vector, so it has no vector of norm one. In a nontrivial Hilbert space, choose $x\ne0$ and normalize $x/\|x\|$. The corrected theorem requires nontriviality. A formal type may legitimately admit the zero space even when a physicist implicitly means a nonempty state space. Making the hypothesis explicit prevents a theorem interface from encoding a stronger, false statement.

References

• Hietala, Kesha, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks, “A Verified Optimizer for Quantum Circuits,” Proceedings of the ACM on Programming Languages 5, POPL (2021), author publication record, arXiv:1912.02250 — a concrete use of formal semantics and reusable correctness proofs.
• Lean Project, Theorem Proving in Lean 4, online book, official text — propositions, proof terms, and mathematical interfaces.
• Lean Project, The Lean Language Reference, “Validating a Lean Proof,” official documentation — statement and dependency checks required beyond a successful elaboration.