Proof Assistant Preview

A proof assistant helps construct a derivation and checks it within a specified formal foundation. To read a quantum development productively, start with the theorem’s mathematical meaning, then inspect its types, assumptions, and library dependencies. Understanding the proof state is more useful than treating a long tactic script as an unexplained certificate. This guide is a workflow, not a claim that the articles in this volume have all been formalized.

Helpful background. Formal Proofs versus Human Proofs separates semantic adequacy from derivation checking; Finite-Dimensional QM Formalization shows a concrete collection of mathematical interfaces.

Definitions and theorem types come before tactics

In dependent-type systems such as Lean and Rocq, a proposition is represented by a type and a proof by a term of that type. Interactive commands and tactics help construct the term. Isabelle commonly presents mathematics in higher-order logic through structured Isar proofs and tactics, with inferences checked through its logical infrastructure. The systems differ in foundations and library organization; a shared mathematical vocabulary does not imply interchangeable source files.

Suppose a declaration concerns a “state.” Read its definition. It may mean a normalized vector, a ray, a positive trace-one matrix, or a positive functional. Likewise a “linear map” might be algebraic, continuous, or partially defined. These are different interfaces, not merely different spellings of an operator.

Before studying a proof, translate its type into ordinary mathematics: identify the scalar field, dimensions, input and output spaces, normalization conditions, and quantifier order. An implicit parameter or automatically supplied structure can carry a crucial assumption such as completeness or finite dimensionality.

The proof state exposes the current obligation

A proof state records local variables, hypotheses, and a goal. Applying a lemma transforms the goal into that lemma’s premises; rewriting replaces an expression using an established equality; introducing a variable or hypothesis handles a universal quantifier or implication. Automation can perform many such steps, but the final obligation must still follow from the available assumptions.

In a channel proof, a goal involving a trace might reduce to cyclicity and a normalization identity. If the map acts on infinite-dimensional operators, that cyclicity lemma must carry its trace-class and boundedness hypotheses. A failed application can reveal a real mathematical gap rather than merely a missing tactic. The trace-class treatment explains the analytic conditions that a formal interface should preserve.

When diagnosing a failure, first check whether the intended statement is true at the available level of generality. Only then decide whether a coercion, notation convention, missing imported lemma, or proof strategy is responsible.

Inspect the dependency assumptions

A successful file check establishes a result relative to its definitions, axioms, imported declarations, and relevant trusted mechanisms. It does not make every imported assumption a proved theorem. In Lean, #print axioms theoremName exposes axiomatic dependencies; a dependency on sorryAx indicates an admitted proof. Here theoremName is a placeholder for the actual declaration being checked. A text search for sorry in one file is weaker because admissions can be imported indirectly.

Lean’s validation documentation also distinguishes proof-producing computation from mechanisms that add compiler-related trust. Rocq provides assumption inspection as well, and its reference manual explains kernel checking of proof terms. The relevant lesson is to record what was trusted and why, rather than count only completed goals.

An axiom is not automatically an error: a development can intentionally work relative to a declared physical or mathematical premise. The claim must then remain an implication under that premise. Adding an unsupported axiom that is the desired conclusion changes the task from proving to assuming it.

Reproduce a result at a fixed revision

A useful formal artifact identifies its source revision, proof-assistant version, library revisions, command or project entry point, and the exact theorem declarations checked. It should distinguish a clean check from a partial run, cached output, or an unexecuted code example. Reproducibility requires the dependencies as well as the visible proof script.

Library documentation can locate candidate results, but a similarly named theorem may have different hypotheses. For example, a finite-dimensional self-adjoint diagonalization theorem is not an unbounded spectral theorem on a general Hilbert space. Inspect the declaration and then use the spectral formalization guide to identify the additional interfaces needed.

This page does not prescribe installing a particular system. For a concrete project, the existing mathematical library, theorem scope, collaborators, and reproducibility requirements should guide that implementation choice.

Exercise: interpret a successful build with an admission

A theorem about all quantum channels checks successfully, but its dependency report includes an admitted lemma asserting positivity of every linear map. Explain both what the checker established and why the claimed quantum result is unsupported.

Solution

The checker established a derivation relative to the admitted assertion. That assertion is false: even multiplication of every matrix by $-1$ is linear and sends a nonzero positive matrix to a negative one. The artifact therefore does not establish the advertised theorem from the intended quantum assumptions. The admission must be removed or replaced by a true lemma with suitable hypotheses, after which the dependent proof must be checked again.

References

• Lean Project, The Lean Language Reference, “Validating a Lean Proof” and “Axioms,” validation, axioms — dependency and trust inspection.
• Nipkow, Tobias, Programming and Proving in Isabelle/HOL, tutorial, 18 January 2026 edition, official PDF — structured proofs, theorem application, and Isabelle/HOL foundations.
• Rocq Development Team, The Rocq Prover Reference Manual, version 9.2, “Core language,” official documentation — kernel checking and elaboration.