Lean Proof-Search Lab Runtime

It searches small Lean theorems for a proof, checks each candidate with the installed Lean toolchain, and reports itself locked when Lean is absent. lean_proof_search_lab_runtime searches small Lean theorems for a proof and checks each candidate with the Lean toolchain that is actually installed. When Lean is not installed it reports itself locked and claims nothing.

Lean compilation and clean-axiom admission

A candidate is kept only when the lean subprocess compiles it with a clean #print axioms set, and the run emits a status, tool state, and per-case breakdown. It takes a directory of fixture cases, runs a bounded tactic search over each toy theorem, hands every candidate script to the lean subprocess, and reads #print axioms on what comes back. A candidate is kept only when Lean compiles it with a clean axiom set. The component emits a result record with a status, a tool state, and a per-case breakdown.

The third outcome is the point: with no lean binary the run neither passes nor fails but reports locked and verifies nothing. The interesting part is the third outcome. A demo that prints a tactic and asserts success is easy to fake. This component instead answers whether a real checker ran and whether a reader can tell that it ran. When the lean binary is missing it does not pass and does not fail: it reports locked and performs no verification.

Purpose

Three ways a loose checker cheats

A cheap "proof found" badge fails three ways: a forwarded proof body, a script leaning on sorry or extra axioms, or a tactic picked from the problem's name. A green badge that says "proof found" is cheap. The hard question is whether the proof was checked by something that could have said no, and whether the result stays honest when the checker is absent. A loose implementation fails in three ways: it forwards a ready-made proof body and calls that a search, it accepts a script that leans on sorry or extra axioms, or it only picks the right tactic because it recognised the problem's name. This component is built to reject all three by recomputation, and to refuse to report a pass at all when Lean cannot be run.

How it works

Wrapper picks the terminal state

The runtime wrapper decides which of three terminal states applies, then delegates the real search to the lab in lean_proof_search_lab.py. The runtime wrapper in organs/lean_proof_search_lab_runtime.py decides which of three terminal states applies, then delegates the real work to the lab in engine_room/lean_proof_search_lab.py.

build_result branches on Lean's presence

build_result branches on lean_available: absent yields _locked_result, present runs evaluate_fixture_dir and reaches tool_present_and_verified only when positives pass, every negative is caught, and no case is unaccounted for. lean_available probes for the binary with shutil.which("lean"). build_result branches on it. If Lean is absent it returns _locked_result: status locked, tool state tool_missing, no cases, verification_performed false. If Lean is present it calls evaluate_fixture_dir, classifies every returned case with _classify_case, and sets the tool state to tool_present_and_verified only when the positive cases pass, every expected negative case is present and rejected, and no case is left unaccounted for. Otherwise the tool state is tool_present_but_failed. run writes the result record, a compact card from result_card, and a validation record to the output directory.

The lab pipeline entry point

Inside the lab, evaluate_fixture_dir runs evaluate_case on each *.json file, which unpacks it and calls the evaluate_lab pipeline. Inside the lab, evaluate_fixture_dir reads each *.json file in the input directory and runs evaluate_case, which unpacks the case and calls evaluate_lab. evaluate_lab is the pipeline, and it runs in this order:

Firewall strips forbidden proof fields

_forward_firewall fails the case with oracle_firewall_violation if any FORBIDDEN_FORWARD_FIELDS carries a value, then strips them so a leaked proof body cannot become forward evidence. First _forward_firewall scans the raw problem rows for any of the FORBIDDEN_FORWARD_FIELDS (candidate_body, ideal_body, repair_body, oracle_body, oracle_needed_premise_ids, provider_text), nested paths included. If any are present with a value, the firewall fails and the whole case fails with kind oracle_firewall_violation. The forbidden fields are stripped before the search sees the problem, so a leaked proof body cannot become forward evidence.

Shape-ordered search checked by Lean

run_and_or_search orders candidate tactics by inferred shape and hands each to check_candidate_with_lean, which rejects sorry, runs the lean subprocess, and selects the first candidate accepted with clean axioms. Then for each cleaned problem run_and_or_search runs a bounded candidate-tactic search. infer_target_shape reads the theorem signature and picks a shape (or_comm, and_comm, and_intro, false_elim, identity_intro, true_intro, exists_zero, equality). _base_candidate_actions orders the tactic scripts with the matching shape first. Each candidate goes to check_candidate_with_lean, which builds a Lean source file, statically rejects any body containing sorry, and otherwise runs the lean subprocess and reads its axioms with _classify_axioms. The first candidate Lean accepts with a clean axiom set is selected; duplicates are pruned by goal hash.

Ablation and axiom taint gate pass

run_blind_policy_ablation renames each problem id and fails on divergent selections, and any axiom taint fails the case, so a pass needs firewall, search, stable ablation, and clean axioms. Finally run_blind_policy_ablation renames each problem id with _rename_problem_id and reruns the policy. If a policy selects a different tactic once the problem is renamed, its selection counts diverge and the ablation fails with kind problem_id_ablation_failure. evaluate_lab also counts axiom-tainted frontier rows; any taint fails the case with kind axiom_taint_detected. The case passes only when the firewall holds, every problem is closed by search, the ablation is stable, and no axiom taint is present.

flowchart TD Probe["lean_available shutil.which(lean)"] Locked["_locked_result tool_missing, no claim"] Firewall["_forward_firewall FORBIDDEN_FORWARD_FIELDS"] Search["run_and_or_search candidate tactic scripts"] Lean["check_candidate_with_lean lean subprocess"] Axioms["_classify_axioms #print axioms clean"] Ablation["run_blind_policy_ablation rename problem id"] Verdict["build_result pass or fail"] Probe -->|absent| Locked Probe -->|present| Firewall Firewall --> Search Search --> Lean Lean --> Axioms Axioms --> Ablation Ablation --> Verdict

The bundle entry never spawns Lean

run_lean_proof_search_lab_runtime_bundle only checks that an exported bundle declares its required files, never spawning Lean, so live verification happens only through run. The bundle entry run_lean_proof_search_lab_runtime_bundle is separate. It checks that an exported bundle declares its required files and never spawns Lean, so its tool state is standalone_contract_not_executed. Live Lean verification only happens through run.

Negative cases

Four planted cheats and their guards

EXPECTED_NEGATIVE_CASES names four planted cheats, each with the guard that must catch it by recomputation rather than a hard-coded expected answer. The wrapper names four planted cheats in EXPECTED_NEGATIVE_CASES, each with the guard that must catch it. Every one must be rejected by recomputation, not by a hard-coded expected answer.

Which guard catches each cheat

A leaked body fails the firewall, a sorry script fails the axiom audit, and a name-reading policy fails the ablation; a verified run needs the positive and all four caught. oracle_field_negative and nested_oracle_field_negative plant a forbidden proof body at the top level and nested inside the payload. Both must fail with oracle_firewall_violation. sorry_axiom_negative submits a script that closes the goal with sorry, and must fail with axiom_taint_detected. memorized_policy_negative submits a policy that only picks the right tactic because it read the problem's name, and must fail with problem_id_ablation_failure once the id is renamed. A run reports tool_present_and_verified only when the honest positive case passes and all four of these are caught.

Prior Art Grounding

Prover, renaming, and leakage discipline

Sign-off rests on the external Lean 4 prover and its #print axioms audit, the ablation borrows renaming discipline from memorisation testing, and the firewall borrows leakage discipline. The engineering lineage is standard proof-checking practice rather than a single cited result. The component checks candidates with the Lean 4 theorem prover as an external subprocess and audits them with Lean's own #print axioms command, so sign-off depends on the prover and not on this code. The problem-id ablation follows the held-out and renaming discipline used to detect memorisation in machine-learning evaluation: if renaming the problem changes the answer, the policy was reading the label. The oracle firewall follows the same idea applied to data leakage, refusing forward fields that would let a ready-made answer stand in for a search.

Validation Result record Path

Running the proof-search fixtures

Run the component over its fixtures, then rerun the corpus checks that read this page: Run the component over its fixtures, then rerun the corpus checks that read this page:

What a pass and a lock mean

A pass means Lean was installed, accepted the toy theorems with clean axioms, and the three guards each rejected their planted defect; no Lean on the path reports locked. A pass means Lean was installed, it accepted the toy theorems with clean axioms, and the firewall, axiom audit, and ablation each rejected their planted defect. If Lean is not on the path the run reports locked and asserts nothing.