Mechanical Proof Checker¶
Automated verifier — instantiates Formal Derivation System Design
Independently re-checks a supplied derivation step by step against the rules and returns a pass/fail verdict plus a certificate that the conclusion lies inside the system's closure.
A Mechanical Proof Checker is the small, trusted verifier of a formal system. Handed a complete derivation and the theorem it claims to establish, it re-runs every step, confirming that each is a legal instance of an inference rule applied to well-formed premises, and that the last line is the claimed conclusion. If every step checks, it accepts and emits a machine-checkable certificate; otherwise it rejects and points at the first bad step. Its defining commitment is independent re-validation of one given proof: it authors no rules, hunts for no system-wide contradiction, and merely records nothing — it renders a verdict, and its verdict is a decision about whether the conclusion lies inside the system's derivable closure.
Example¶
A proof assistant in the mould of Lean or Coq lets mathematicians build proofs with a large, sophisticated, and inevitably bug-prone tactic engine. What makes the result trustworthy is not that engine but a tiny kernel — often only a few hundred lines — that plays the checker's role. When a user finishes a proof, the enormous tactic machinery hands the kernel a finished proof object; the kernel re-checks it from scratch against the primitive inference rules, ignoring how it was found. A proof that the tactics were "sure" of but that does not actually reduce to a valid derivation is rejected by the kernel. Trust concentrates in the small checker rather than the big generator — the de Bruijn criterion — so a mathematician need only believe a few hundred lines, not the whole system.
How it works¶
- Take proof plus claim. The input is a full derivation (typically from a Proof Tree or Derivation Log) and the theorem it purports to prove.
- Re-derive independently. Each step is re-checked as a licensed rule instance over well-formed expressions — the checker recomputes rather than trusting the producer's assurance.
- Decide closure membership. Acceptance means the claimed conclusion is genuinely reachable by the rules from the axioms — a verdict on whether it lies inside the derivable closure.
- Emit a certificate; keep the base small. A passing check yields a compact, re-checkable certificate, and the whole checker is kept as small as possible so that what must be trusted is minimal.
Tuning parameters¶
- Trusted-base size — how small the checker's kernel is. A smaller kernel is more trustworthy but supports fewer conveniences; a larger one is easier to use but harder to believe.
- Check completeness — full re-derivation of every step vs. spot-checking. Full checking is airtight but slower; sampling is fast but leaves gaps.
- Certificate detail — how much the emitted certificate records for later independent re-checking. Richer certificates travel better; leaner ones are cheaper to produce.
- Producer independence — whether the checker shares code with the proof generator. Independence is the whole source of trust; shared code quietly undermines it.
When it helps, and when it misleads¶
Its strength is converting "trust the tool" into "check the proof": you no longer have to believe a vast, opaque generator — you believe a small verifier that re-examines the result. That is what lets enormous machine-generated proofs be relied upon at all.
Its failure mode is a boundary it cannot cross: the checker certifies validity relative to the declared rules and axioms. Feed it a system with wrong or too-strong axioms and it will happily certify a flawless derivation of a claim that is false in the world — garbage in, certified garbage out.[n1] The classic misuse is a checker that shares implementation with the prover, so a bug in common code passes both silently; the independence that makes checking meaningful is lost. The guarding discipline is to keep the trusted base small and genuinely independent, and to remember that formal validity is not soundness-for-the-world — that gap is patrolled by metatheory and interpretation, not by the checker.
How it implements the components¶
derivation_trace_record— it validates a supplied trace and emits a compact, machine-checkable certificate: a re-verifiable record that the derivation holds up.closure_boundary— its accept/reject verdict is a decision about closure membership: whether the claimed conclusion is genuinely derivable inside the system.
It verifies one supplied proof; it does not maintain a library of derivations (exemplar_derivation_suite — that is the Proof Tree or Derivation Log, whose recorded traces this checker re-validates) and it does not sweep the whole system for a derivable contradiction (consistency_guardrail — that system-global hunt belongs to the Consistency and Contradiction Test).
Related¶
- Instantiates: Formal Derivation System Design — provides independent, mechanical verification of individual derivations.
- Consumes: Proof Tree or Derivation Log supplies the derivation to check; Inference Rule Calculus supplies the rules to check it against.
- Sibling mechanisms: Formal Grammar Specification · Well-Formedness Linter · Axiom Schema Catalog · Inference Rule Calculus · Rewrite or Transition Rule Engine · Proof Tree or Derivation Log · Metatheory Review Checklist · Consistency and Contradiction Test · Formal-System Change-Control Workflow
Editorial Notes¶
Form Classification¶
Form family: Assessment, Review & Assurance
Rationale: Mechanical Proof Checker operates as a bounded evaluation of existing evidence or work that produces a finding or disposition because it independently re-checks a supplied derivation step by step against the rules and returns a pass/fail verdict plus a certificate that the conclusion lies inside the system's closure.
Independent corroboration: The frozen evidence defines Mechanical Proof Checker as 'Independently re-checks a supplied derivation step by step against the rules and returns a pass/fail verdict plus a certificate that the conclusion lies inside the system's closure', so its operative form is Assessment, Review & Assurance.
Nearest alternative: Analysis, Modeling & Optimization — The checker re-derives steps computationally, but its purpose is a bounded independent assurance verdict on a supplied proof.
Review outcome: Independent reviewer agreement; medium confidence.
Origin Attribution¶
Primary origin: Computer Science & Software Engineering
Origin pattern: Cross-disciplinary synthesis
Present-day reach: Multi-domain
Rationale: Automated proof checking arose in theoretical computer science and formal methods.
Related originating lineages:
- Mathematics — Formal logic and axiomatic proof systems supply the derivation rules and closure concept.
Review resolution: Both independent reviews place the primary provenance in computer_science. The queued differences (domain_reach_disagreement) concern secondary metadata, not primary lineage. The final retains mathematics only where a reviewer supplied a formative-lineage rationale; downstream use or broad applicability by itself is not treated as origin. origin_mode=cross_disciplinary_synthesis because the supplied rationales identify formative contributions that are composed in the mechanism's present form. domain_reach=multi_domain records established application breadth separately from provenance. confidence=high preserves the more cautious evidence assessment. encyclopedia_synthesis=false records whether either reviewer identified deliberate corpus-level composition.
Review outcome: Reconciled after independent review; high confidence.
Notes¶
[n1] The de Bruijn criterion holds that a proof-checking system is trustworthy if the correctness of any accepted proof depends only on a small, independently checkable kernel. It concentrates trust in a tiny verifier — but only for validity relative to the declared rules, never for the truth of the axioms themselves. ↩