Engine Room Lean Proof Search Lab

Component runs tiny

This component runs tiny public Lean statements through a small shape-driven proof search and reports which ones the installed lean kernel actually closes on a real run. This component runs tiny public Lean statements through a small proof search and reports which ones the installed Lean kernel actually closes. It reads a group of theorem statements, proposes candidate tactic bodies from the shape of each goal, writes each candidate to a temporary .lean file, and runs the real lean executable over it.

Search loop is

A search loop is easy to fool by leaked answers, id memorisation, or a sorry-backed file, so this component is built mostly to refuse that false credit rather than to score wins. A search loop is easy to fool. It can copy a proof out of an answer field, learn to map a problem id to a stored tactic, or compile a file that leans on sorry. Each of those returns a green result that means nothing. This component is built mostly to refuse that false credit, not to score wins.

Each fixture case yields one result record bundling the firewall report, search trace, statement-only table, ablation report, and a single pass or fail with its failure_kind. The output is one result record per fixture case: the firewall report, the search trace, the statement-only table, the ablation report, and a single pass or fail with a named failure_kind.

Purpose

Trust, not search, is the hard part

The hard part of a proof-search tool is not finding a proof but trusting that a reported success was earned rather than leaked or memorised. A loose lab that only counts closed goals cannot tell an earned proof from a smuggled one.

Generation proposes, Lean decides

For each statement it asks whether the search actually closed the goal and whether the installed Lean kernel agrees the proof depends on no axioms, keeping generation cheap and untrusted. This component answers one question per statement: when a tiny public theorem is reported solved, did the search actually close it, and does the installed Lean kernel agree the proof depends on no axioms. Candidate generation stays cheap and untrusted. All authority moves to the kernel. Generation proposes, Lean decides.

How it works

The two entry points

evaluate_lab runs the pipeline for one group of problems in a fixed order, while evaluate_fixture_dir scores every *.json case against the status and failure_kind its fixture expects. evaluate_lab runs the pipeline for one group of problems in a fixed order. evaluate_fixture_dir loads every *.json case in a directory and runs them through evaluate_case, which compares the observed status and failure_kind against the values the fixture expects.

The order of operations inside evaluate_lab:

1. _forward_firewall walks every input row first. _forbidden_field_paths recurses through nested maps and lists looking for any of the fields in FORBIDDEN_FORWARD_FIELDS: candidate_body, ideal_body, repair_body, oracle_body, oracle_needed_premise_ids, provider_text. If any is present and non-empty the firewall reports fail and the search never runs. This is what stops an answer being handed in as a hint.
2. _public_problem strips those forbidden fields, then _problem_from_mapping builds a LeanProblem from what remains. infer_target_shape reads the theorem signature and classifies the goal, for example Or p q -> Or q p becomes or_comm and a = goal becomes equality.
3. For each problem run_and_or_search builds candidate tactic bodies with _base_candidate_actions. These are deterministic templates keyed by shape: or_comm draws an Or.inl / Or.inr case split, equality draws rfl, and so on. It dedupes candidates by a goal hash, calls check_candidate_with_lean on each, and stops at the first accepted one.
4. run_statement_only_hammer runs a second pass that uses only statement-shaped candidates. It records an action value table with a posterior score per tactic and never credits an adapter candidate or a repair body.
5. run_blind_policy_ablation renames each theorem and its id through _rename_problem_id, picks an action for both the original and the renamed problem, and compares them with _policy_signature. It passes only when the chosen action, the action-kind counts, and the success counts all match. A policy that had secretly keyed on the id changes its choice under the rename and fails here.

The kernel run is the authority

check_candidate_with_lean accepts a candidate only when lean exits zero, the source carries no sorry, and #print axioms confirms the theorem depends on no axioms. check_candidate_with_lean is where a candidate becomes a fact or nothing. _statement_source assembles the .lean file and appends #print axioms <theorem>. If the body contains sorry the function static-rejects it before Lean ever runs. Otherwise a cached single-flight helper writes the file to a temporary directory and runs lean on it under a timeout. _classify_axioms reads the process output: a candidate is accepted only when the process exits zero and the output says the theorem "does not depend on any axioms", with no sorry in the source. A compiled file that depends on axioms is not accepted.

Folding the passes into one status

evaluate_lab folds the three passes into one status that fails on an empty set, firewall violation, unclosed goal, axiom taint, or failed ablation, naming the reason in failure_kind. evaluate_lab then folds the three passes into one status. It fails on an empty problem set, a firewall violation, any problem the search or hammer did not close, any axiom taint, or an ablation that did not pass, and names the reason in failure_kind. main exposes the two commands, evaluate-lab and evaluate-fixtures, and returns a non-zero exit code when the status is fail.

flowchart TD A["Group of theorem statements"] --> B["_forward_firewall reject leaked answer fields"] B --> C["run_and_or_search shape-keyed tactic candidates"] C --> D["check_candidate_with_lean run lean subprocess"] D --> E["_classify_axioms reject sorry or axiom taint"] C --> F["run_statement_only_hammer statement-only value table"] F --> G["run_blind_policy_ablation rename ids, recheck policy"] E --> H["evaluate_lab result record"] G --> H

Negative cases

Public fixtures name

The public fixtures name four failures and one pass, and each fixture states the failure_kind it expects. The public fixtures name four failures and one pass, and each fixture states the failure_kind it expects:

• oracle_field_negative: a row carries a forbidden answer field, so the firewall fails with oracle_firewall_violation and no search runs.
• nested_oracle_field_negative: the forbidden field is buried inside a nested structure, and _forbidden_field_paths still finds it. Same failure_kind.
• memorized_policy_negative: an id-conditioned policy is caught by the rename ablation and fails with problem_id_ablation_failure.
• sorry_axiom_negative: a candidate body carries sorry, so the axiom audit fails the case with axiom_taint_detected.
• positive_symbolic_lab_pass: tiny statements close under the shape-keyed search with clean axioms, the firewall is clean, and the ablation is stable.

Prior Art Grounding

Tactic automation with kernel authority

The design follows interactive theorem proving where automation proposes small tactic scripts and the kernel stays the authority, echoing Lean 4 tactics and Isabelle Sledgehammer's replay discipline. This component follows the interactive-theorem-proving pattern where automation proposes small tactic scripts and the kernel stays the authority. Theorem Proving in Lean 4 is the direct precedent for tactic-structured proof construction. The statement-only pass is adjacent to hammer workflows such as Isabelle Sledgehammer, where an outside search suggests steps but the proof assistant must replay the result. Here candidate generation is fixture behavior and the lean run plus the #print axioms audit decide what counts.

Validation Result record Path

Run the public fixture matrix directly:

PYTHONPATH=src python3 -m microcosm_core.engine_room.lean_proof_search_lab evaluate-fixtures \
  --input fixtures/first_wave/engine_room_lean_proof_search_lab/input \
  --json

Reader-verifiable check is

The reader-verifiable check is the focused test plus the corpus parity check. The reader-verifiable check is the focused test plus the corpus parity check:

PYTHONPATH=src ./repo-pytest tests/test_engine_room_lean_proof_search_lab.py -q
cd microcosm-substrate && PYTHONPATH=src ../repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus

What a pass means here

A pass means only that the public fixture behavior and the bundle projection are reproducible, admitting nothing into the shared registry and authorizing no launch. A pass means only that the public fixture behavior and the bundle projection are reproducible. It does not admit a component into the shared registry or include launch operations.