How the checking works

The useful architectural distinction is between finding a proof and checking a proof. Search can be complicated, heuristic or AI-driven while acceptance follows fixed formal rules. The separation makes proof search replaceable. It does not remove the need to inspect the specification being proved.

From a mathematical sentence to a checked object

A typical development passes through five stages:

1. Specify. Choose domains, definitions, hypotheses and conclusion.
2. Elaborate. Resolve notation, implicit arguments and overloaded operations into a precise internal expression.
3. Construct. Supply proof terms, structured steps, tactic scripts or automated search.
4. Check. Apply the system’s formal inference or typing rules under the declared assumptions.
5. Interpret. Compare the accepted statement and derivation with the mathematical claim and explanation.

The architecture of the fourth stage varies. The first and fifth stages are part of every serious mathematical use. A formalizer can choose a different theorem before the checker sees anything, just as a program can satisfy a wrongly written specification.

In dependent type theory, a proposition can be represented as a type. A proof is a term of that type. For instance, a proof of $𝑃\Rightarrow 𝑄$ behaves like a function taking evidence for $𝑃$ to evidence for $𝑄$. A dependent type may also mention a value: a vector type indexed by its length lets an append function express its output length in its type. Lean, Rocq and Agda use this connection between proofs and typed programs.¹²³

LCF-style systems use another mechanism. Their theorem values belong to an abstract type whose normal construction operations implement trusted inference rules. An automation procedure may choose the wrong inference and fail, but it cannot ordinarily manufacture a theorem merely by returning a plausible string. Isabelle and the HOL family follow this tradition; declared axioms and oracle mechanisms remain separate trust extensions.⁴⁵

Compare the proof surfaces

This table describes the main layers, rather than a complete security audit. Mizar’s soft types organize set-theoretic predicates; they do not give it the same foundation as dependent type theory. Its historical architecture lacks the small LCF-style kernel described above.⁶

Lean’s tactics are programs that construct proofs. Rocq’s Gallina definitions can also describe executable algorithms, with extraction to other languages. Isar’s declarative steps can invoke operational proof methods. These systems therefore mix declarative and procedural activity at different layers.⁷⁸⁹

A correct replacement proof can leave a bad argument untouched

Let $𝐴=\left({𝑎}_{𝑖𝑗}\right)$ be a real symmetric matrix. The statement $tr\left({𝐴}^2\right)\ge 0$ has a short proof:

The first equality expands matrix multiplication and trace. The second uses symmetry. A different proof diagonalizes $𝐴$ and sums the squares of its eigenvalues. Both establish the same conclusion.

If an AI receives a flawed diagonalization argument and instead produces the first proof, machine checking can accept the result. Acceptance does not validate the flawed argument supplied as input. If the AI also changes the statement, acceptance establishes only the changed claim. Statement fidelity and argument fidelity therefore need separate evaluation. This example is mathematical reasoning presented here, not a report of a new theorem or a prover execution.

Automation has more than one trust boundary

Rocq’s MathComp uses reflection: prove a connection between a proposition and an executable test, then use verified computation to establish the proposition. For finite structures, this can turn logical reasoning into manageable calculation. The four-color and odd-order projects made this approach a sustained mathematical practice.¹⁰¹¹

Isabelle’s Sledgehammer sends suitable problems to external provers and normally returns Isabelle proof text that reconstructs the result. External success and successful reconstruction are distinct events. The reconstructed proof supplies the ordinary kernel-based justification; a solver’s assertion alone does not.¹²

Agda’s --safe option constrains the import closure and disables postulates and several ways to bypass important checks. Cubical Agda adds trusted computational primitives supporting paths and derived univalence. These are stronger contracts than treating every permissive Agda session as equally assured. They still rely on the implemented checker.¹³¹⁴

Arend’s metas can construct expressions that are typechecked, and its language permits explicitly declared axioms. Its Java extension API also allows code to run during type checking. This survey did not establish an Agda-like global safe mode or independently audit the extension trust boundary.¹⁵¹⁶

Libraries are part of the practical language

The available definitions determine which statements are convenient to write. The available theorems determine how much infrastructure an author must build. The community determines which conventions receive review and ongoing maintenance.

Mathlib offers shared structures and an integrated contribution process. MathComp supplies a coherent reflective mathematical style within the broader Rocq ecosystem. AFP publishes Isabelle developments with review. MML manages article environments and library submissions. Agda has several distinct libraries, including the standard library, TypeTopology and the cubical library; Arend’s principal mathematical collection is arend-lib.^171819202122

HOL Light’s OCaml proof programs, HOL4′s Standard ML theories and Metamath’s explicit substitution proofs illustrate further choices. Metamath’s principal databases use several independent verifiers. That checks agreement on a formal artifact; it does not mechanically settle its informal interpretation.²³²⁴²⁵

What a useful verification receipt contains

For a serious result, record the exact statement, its definitions, allowed assumptions, prover and library versions, and the checking result. Record separate evidence for the link to the informal mathematics. Recent Lean release notes document soundness defects discovered through adversarial testing, including one shared by an independent checker. “Small kernel” and “two checkers” are useful engineering properties, not unconditional guarantees.²⁶

Problem space

• Understand representation: report 3 compares foundations, equality and mathematical interfaces.
• Assess a translation: audit the statement separately from whether the formal proof follows the submitted argument.
• Terminus: the architecture explains what acceptance means; selecting a project requires domain-specific evidence.