Proof Assistant Script¶
Verification software — instantiates Contradiction-Closure Proof
Encodes an indirect proof as code checked by a trusted kernel, so every inference and the discharge are mechanically verified and each classical axiom is forced into the open.
Proof Assistant Script is an indirect proof rewritten as executable code inside an interactive theorem prover, where a small trusted kernel accepts the proof only if every step type-checks. Its distinctive property is that correctness is no longer a matter of any human's care: the machine will not let the script by_contra its way to a conclusion unless the derivation genuinely reaches falsum and the assumption is legitimately discharged, and — the sharpest feature for this archetype — it forces the logic into the open. In a constructive foundation, invoking classical reasoning (double-negation elimination, excluded middle) is not free; it appears as an explicit axiom the script must name, so the exact place where the proof leans on classical closure becomes a visible line of code rather than a silent assumption. The script does not judge whether the theorem is worth proving or whether a direct proof would read better; it judges, mechanically and unforgivingly, whether the proof is valid in a declared logic.
Example¶
An engineer wants to be certain that a small routing table can never produce a forwarding loop, and encodes the claim in a proof assistant such as Lean or Coq. She states the theorem, then writes the indirect argument: intro the assumption that a loop exists, by_contra, and derive that some node both precedes and follows itself in the ordering — a contradiction with the ordering's irreflexivity, closed by exact. The kernel checks it. When she uses classical case analysis on whether a node is reachable, the system requires her to open the Classical namespace; that dependency is now recorded in the proof term. Running the assistant's axiom-tracking command lists exactly which classical axioms the proof consumed.
The payoff is twofold. First, the proof is machine-verified — no reviewer needs to trust her step-by-step reasoning. Second, the classical dependence is explicit: anyone who needs a constructive result can see precisely which lemma to reprove, because the tool marked it. The famous demonstration that this scales is real: the four-colour theorem was fully verified in Coq[1], settling doubts that hand-checking of its cases never could.
How it works¶
- Encode the statement and the assumption. The theorem becomes a typed proposition; the indirect step introduces the negation as a hypothesis via the prover's contradiction tactic.
- Derive under kernel check. Each tactic corresponds to an inference the kernel re-checks; a step that does not follow is simply rejected, so the derivation cannot cheat.
- Declare the foundation. The proof lives in the assistant's logic (typically intuitionistic type theory), which fixes what is provable without extra axioms and bounds the result's meaning.
- Surface classical use. Any appeal to classical principles imports a named axiom, and the tool can report the full axiom footprint, marking every place the proof exceeds constructive logic.
Tuning parameters¶
- Foundation and library — which prover and axiom base (constructive core, classical extension). A richer base shortens proofs but widens the trusted footprint.
- Automation level — hand-written tactics versus heavy automation/decision procedures. Automation saves labour but can obscure which axioms a proof actually pulled in.
- Axiom-tracking strictness — whether the build fails on any classical axiom or merely reports it. Strict mode guarantees constructivity; lenient mode allows it knowingly.
- Trusted-kernel size — how minimal the kernel is kept. A smaller kernel is more trustworthy but supports fewer conveniences.
When it helps, and when it misleads¶
Its strength is that it removes human trust from the inner loop: the derivation is checked mechanically, the discharge cannot be faked, and — uniquely useful here — the logic boundary is not asserted but computed, since every classical axiom the proof used is enumerable. It is the strongest available guard against the archetype's "used classical closure in the wrong logic" failure.
Its failure mode is that the machine verifies the encoding, not the world: a script can be flawlessly checked yet prove the wrong theorem because the formalization mis-states the claim or the definitions drift from their informal meaning, and a large trusted base or an unsound axiom quietly widens what "checked" means. Mechanization can also make an ugly proof pass without anyone asking whether a clearer one exists. The guarding discipline is to review the statement and definitions by hand even when the proof is machine-checked, and to keep the axiom footprint and kernel as small as the problem allows.
How it implements the components¶
Proof Assistant Script realizes the mechanically-verified-derivation side of the archetype:
derivation_path— the tactic script is the derivation, re-checked step-by-step by the kernel so no inference is taken on trust.scope_and_logic_boundary— the prover's foundation fixes the logic the proof holds in, making the boundary a declared, enforced property of the build.logic_exception_marker— every appeal to a classical principle imports a named axiom, so the tool marks exactly where the proof exceeds constructive logic.
The script verifies a constructed proof but does not render the human judgement that a direct proof would be preferable, nor keep the narrative reviewer's record (constructive_alternative_note, proof_audit_record) — that is Peer Proof Review; the machine checks validity, the review judges fit.
Related¶
- Instantiates: Contradiction-Closure Proof — supplies the mechanical verification and explicit logic footprint the archetype's rigor and scope invariants demand.
- Consumes: Natural Deduction Proof Tree — the hand-level derivation the script formalizes into kernel-checked code.
- Sibling mechanisms: Reductio Proof Template · Natural Deduction Proof Tree · Assumption Ledger · Contradiction Search Checklist · Minimal Unsat Core Analysis · Case-Split Elimination Table · Peer Proof Review · Unsatisfiability Certificate
Editorial Notes¶
Form Classification¶
Form family: Assessment, Review & Assurance
Rationale: Proof Assistant Script operates as a bounded evaluation of existing evidence or work that produces a finding or disposition because it encodes an indirect proof as code checked by a trusted kernel, so every inference and the discharge are mechanically verified and each classical axiom is forced into the open.
Independent corroboration: The frozen evidence defines Proof Assistant Script as 'Encodes an indirect proof as code checked by a trusted kernel, so every inference and the discharge are mechanically verified and each classical axiom is forced into the open', so its operative form is Assessment, Review & Assurance.
Nearest alternative: Representation, Specification & Plan — Proof Assistant Script includes features of a static representation, map, specification, schema, or prospective plan that externalizes information, but its defining operation is a bounded evaluation of existing evidence or work that produces a finding or disposition.
Review outcome: Independent reviewer agreement; medium confidence.
Origin Attribution¶
Primary origin: Computer Science & Software Engineering
Origin pattern: Cross-disciplinary synthesis
Present-day reach: Specialized
Rationale: Proof Assistant Script is most plausibly rooted in the computer_science tradition because its characteristic form depends on algorithms, data structures, formal interfaces, and software-system practice. The assignment tracks that formative lineage, not the many settings in which the mechanism can now be applied.
Related originating lineages:
- Mathematics — The mathematics tradition materially shaped Proof Assistant Script through its own practice of formal definition, proof, mapping, and quantitative structure.
- Philosophy — The philosophy tradition materially shaped Proof Assistant Script through its own practice of logic, argument, normative analysis, and conceptual distinction.
Review outcome: Independent reviewer agreement; high confidence.
References¶
[1] Gonthier, G. "Formal Proof—The Four-Color Theorem". Notices of the American Mathematical Society 55(11): 1382–1393 (2008). Documents a large-scale, fully Coq-verified proof of the Four-Color Theorem. registry ↩