Theorem-Prover-Guided Search¶

Proof-search tool — instantiates Computability Boundary Mapping

Uses an automated or interactive prover to search for and mechanically check the proof or certificate a boundary claim rests on, recording the verified guarantee and any open residue.

Theorem-Prover-Guided Search hands the search for a boundary claim's proof to an automated or interactive prover — an SMT solver, a SAT engine, a proof assistant — and keeps only what the prover can mechanically certify. Rather than a human arguing that a decision procedure is correct or a problem impossible, the prover searches the space of proofs and, on success, emits a machine-checkable certificate; on failure it does not bluff — it returns the exact open goal it could not close. Its defining move is mechanisation paired with honesty about the residue: because proof-search for rich logics is itself only semi-decidable, the tool may not terminate with a verdict, and it reports that gap explicitly as an unproven obligation rather than an implied success.

Example¶

A team wants to establish that a small lock-acquisition protocol can never deadlock. They encode the protocol's state transitions and the "no deadlock" property for an SMT solver and ask it to prove the property holds across all reachable states, or to produce a counterexample. The solver searches; for the bounded model it discharges the obligation and emits a proof certificate that a separate, simple checker can re-verify independently — that certificate becomes the guarantee record the team publishes. For an unbounded, parameterized version — any number of threads — the solver cannot close one inductive step within its budget and returns that specific open goal. The team records it as residual uncertainty: "deadlock-freedom proven for the bounded model; the parameterized case is an open obligation." Nothing is claimed that the machine did not check, and the gap is named rather than glossed.

How it works¶

Formalize the claim — a decision procedure's correctness, or an impossibility — as a machine-statable goal.
Drive a prover to search for a proof or a counter-model.
On success, retain the checkable certificate (not merely the prover's say-so) as the guarantee record.
On timeout or an unclosable goal, capture the exact open obligation as residue.

Trust comes from an independent checker re-verifying the certificate, so the search engine itself need not be trusted — only the small checker that reads its output.

Tuning parameters¶

Prover class — SAT versus SMT versus a full interactive assistant; more expressive provers reach harder claims but are less automatic and less likely to terminate.
Search budget — a ceiling on time, memory, or proof depth; a bigger budget closes more goals, though the underlying search may still never halt.
Automation vs. guidance — fully push-button versus human-supplied lemmas and tactics; guidance closes goals the search cannot find alone, at the cost of human effort.
Certificate strictness — whether a result must ship a re-checkable proof object or the prover's bare verdict is accepted; strict certificates buy independent trust.
Residue granularity — how precisely an unclosed goal is reported (the whole claim versus the exact subgoal); finer residue tells you precisely what remains to prove.

When it helps, and when it misleads¶

Its strength is that it delivers machine-checked guarantees no hand proof can match for trust, and it is honest by construction — surfacing exactly what it could not prove rather than overclaiming.

Its failure modes come from the boundary it lives on. Proof-search for rich theories is only semi-decidable, so a non-answer is common and means "not proven," never "disproven"; and a false sense of safety creeps in when the formalization is wrong — the prover certifies the model you gave it, not reality — or when the prover's bare word is trusted without an independent checker.^[1] The classic misuse is reading a timeout as "probably fine," or shipping a "verified" badge backed by a certificate nobody re-checked. The discipline is to re-check every certificate with an independent checker and to treat residue as an open obligation, not a rounding error.

How it implements the components¶

Theorem-Prover-Guided Search fills the mechanical-guarantee side of the archetype — the components a certifying search produces:

computability_guarantee_record — on success it produces a machine-checkable certificate, and that independently re-verifiable artifact is the guarantee record the boundary claim rests on.
uncertainty_residue — when the search cannot close a goal within budget, it captures the exact unproven obligation as explicit residue, so the gap is recorded rather than hidden.

It does not design the reduction or decision procedure it tries to prove — that is Many-One Reduction Proof and Constructive Algorithm and Correctness Proof — and it does not perform the independent re-checking of its own certificate, which Proof Checking owns; the search proposes, the checker disposes.

Instantiates: Computability Boundary Mapping — mechanises the search for the proof a boundary claim needs, and records honestly what it could not close.
Consumes: the formalized goal from Constructive Algorithm and Correctness Proof or Many-One Reduction Proof; its certificate is re-verified by Proof Checking.
Sibling mechanisms: Many-One Reduction Proof · Proof Checking · Constructive Algorithm and Correctness Proof · Enumeration and Dovetailing · Computational Complexity Analysis

Notes¶

The tool's trust boundary is subtle and worth stating plainly: you trust the checker, not the search, which is why a small re-checkable certificate matters far more than the prover's reputation or its heuristics. And the guarantee is always about your formal model — a faithful proof of a wrong encoding is a valid proof of the wrong thing, so the formalization deserves as much scrutiny as the theorem.

References¶

[1] Validity in first-order logic is semi-decidable but not decidable: a complete proof system can enumerate all valid formulas, so a search eventually finds a proof if one exists, but no procedure can in general certify that no proof exists — which is why a prover-guided search may exhaust its budget with the question still open. ↩