Skip to content

Proof Checking

Verification review — instantiates Computability Boundary Mapping

Independently re-verifies a decidability or impossibility proof step by step, so the boundary claim rests on a checked argument rather than on its author's authority.

A boundary claim — "this class is decidable," "no algorithm can solve that" — is only as trustworthy as the argument behind it, and arguments about computability are exactly where subtle gaps hide. Proof Checking produces no new result; it takes an existing proof and re-derives every inference against the rules, mechanically, until either every step is discharged or a gap is exposed. Its defining move is to reduce trust to something small and auditable: instead of believing the author, you believe a compact checker that has re-examined each link in the chain. It is the mechanism that turns "we think this is proved" into "this is checked, and here is exactly what it assumes."

Example

A configuration-language standards group receives a member's proof that well-typedness for the language is decidable, alongside a proposed algorithm. Rather than trust the write-up, they encode the statement in a proof assistant and let its kernel re-check every lemma. Most steps pass. But the checker refuses to close one lemma: the termination argument silently assumed the type graph is acyclic, which the language does not guarantee. The proof is not wrong so much as narrower than claimed — it establishes decidability only for the acyclic fragment. That single flagged assumption, surfaced before anything shipped, redraws the guarantee the group is willing to publish.

How it works

Checking is not searching: the mechanism is given a proof and only validates it, which is what makes it cheap and trustworthy where proof discovery is expensive or undecidable. It re-derives each inference from the previous ones under a fixed rule set, confirms the stated theorem is the one actually proved (not a weaker cousin), and forces every premise into the open — each must be either proved in turn or explicitly declared an axiom. Trust collapses onto a small, independently auditable kernel rather than the full proof, so a reader need only trust the checker, not the prover.

Tuning parameters

  • Kernel trust base — how small and audited the trusted core is. A tiny kernel is more believable but demands that everything be encoded down to it; a larger trusted base is easier to use but asks for more faith.
  • Formalization fidelity — how faithfully the informal claim is translated into the checker's logic. A loose translation can "verify" a statement that is not the one anyone cares about.
  • Assumption strictness — whether unproved lemmas may be admitted as axioms or must themselves be discharged. Stricter settings catch more hidden dependence but cost more effort.
  • Automation depth — how much routine reasoning the checker may close automatically versus requiring spelled-out steps; more automation is faster but widens what you must trust.

When it helps, and when it misleads

Its strength is converting "trust the author" into a mechanically checkable object and dragging every hidden assumption into daylight — precisely the assumptions that make a computability claim narrower than it looks. Its central failure mode is that it verifies the formalized statement, not reality: a faithful-looking but subtly wrong formalization passes cleanly, so a checked proof of the wrong theorem carries all the authority of a right one. The classic misuse is re-checking your own proof inside the same frame that produced the error, or quietly formalizing the conclusion you wanted. The discipline that guards against this is an independent formalization plus a small audited kernel — the de Bruijn criterion[1], which is why trustworthiness is measured by kernel size, not by how much the checker automates.

How it implements the components

  • independent_proof_review — its core act: an independent, mechanical re-derivation of every inference in the submitted proof.
  • assumption_register — it forces each premise into the open and confirms it is either discharged or explicitly declared, producing the ledger of what the boundary claim actually rests on.

It does not produce the proofs it checks — the constructive witness comes from Constructive Algorithm and Correctness Proof and the impossibility certificate from Diagonalization Impossibility Proof; Proof Checking only validates them.

Notes

Proof Checking validates the argument, not the world: it can certify a flawless proof about a model that fails to match the deployed system. Pairing it with an explicit assumption register is what keeps that gap visible — a checked proof plus an unexamined modelling assumption is still a way to be confidently wrong.

References

[1] The de Bruijn criterion — a proof assistant is trustworthy to the extent its soundness rests on a small, independently auditable kernel that re-checks every step, rather than on the mass of automation built above it. ↩