proofrunner

ProofRunner is an evidence-gated execution engine for AI-assisted Lean 4 formalization.

LLMs propose. The Lean kernel verifies. Humans safeguard intent.

Large language models can generate Lean code, but they cannot be trusted to declare their own success. A proof that an LLM claims is complete is just another prediction. A proof accepted by the Lean kernel is an independently verifiable mathematical fact. proofrunner exists to enforce that distinction.

Rather than trusting an agent’s narration, proofrunner trusts only evidence. AI agents work through pre-approved units of formalization called bricks, while a deterministic verifier decides whether each attempt actually satisfies the specification. Kernel-verified lemmas are committed automatically. Definitions and other design-critical artifacts pause for explicit human approval. Everything else is rejected before it can reach your repository.

The result is an agentic workflow where progress is measured by independently verifiable artifacts instead of model confidence. The agent writes proofs. The kernel establishes correctness. Humans retain authority over mathematical intent and design.

The trust boundary

The agent drives the loop, but the harness never trusts the agent's narration. submit_attempt requires:

• the literal build diagnostics for the proof file, and
• the literal textual output of #print axioms <decl> (the 'NAME' depends on axioms: [...] form, generated via a scratch file).

The harness re-reads the proof file from disk itself. Summaries, JSON tool blobs, or paraphrases of any of these are unparseable by design and get rejected, which burns an attempt. This is not an inconvenience; it is the point. In early use, this exact guard caught a real malformed submission (tool JSON substituted for the #print axioms text) and rejected it rather than committing garbage.

The four checks

Every attempt must pass all four:

1. Zero errors. No error: in the build diagnostics.
2. No sorry. Neither the proof file nor the diagnostics contain sorry.
3. Axiom whitelist. #print axioms reports a subset of {propext, Classical.choice, Quot.sound}. Any sorryAx or custom axiom fails. Unparseable input fails.
4. Statement byte-match. The declaration in the file, captured from def|theorem|lemma|abbrev <decl_name> up to the first :=, must match the spec's target after NFC normalization and whitespace collapse. This pins what was proved to the approved spec, so an agent cannot silently prove a weaker statement under the same name.

Checks 1-3 stop unfinished or axiom-smuggled proofs. Check 4 stops the subtler cheat: a real, kernel-clean proof of the wrong theorem.

Gates

Gate	Applies to	On verified attempt
HARD	definition, recon, or any brick with design_critical: true	Parks at AWAITING_APPROVAL; a human calls approve before it commits. Dependents stay blocked.
SOFT	lemma	Auto-commits (staging only the proof file, never git add -A).

The asymmetry is deliberate. A wrong lemma is caught by the kernel. A wrong definition is not: the kernel will happily verify a perfect proof about the wrong object. Definitions and design choices are where formalization projects actually go wrong, so they stay human-gated.

Architecture

 spec files (JSON, human-authored, loaded once at startup)
      |
      v
 +-----------+   next_brick    +-----------+
 |   DAG     |---------------->|  agent    |  edits proof file,
 | scheduler |                 | (LLM/MCP) |  builds, runs #print axioms
 +-----------+                 +-----------+
      ^                             |
      |                             | submit_attempt(literal outputs)
      |                             v
 +-----------+  replay   +----------------------+
 |  ledger   |<----------|  verifier (4 checks) |
 | (JSONL,   |  events   +----------------------+
 |  append-  |              |            |
 |  only)    |          REJECTED      VERIFIED
 +-----------+          (burns an    /        \
      |                  attempt)  SOFT       HARD
      |                             |           |
      v                        auto-commit   parks for
 git auto-commit                            human approve()
 (proof file only)

State is replayed from the append-only ledger at startup, so the harness resumes exactly where it stopped. Specs and the proof-file path are read once at startup; changing them requires a server restart, so a running session cannot have its targets swapped underneath it.

Quickstart

Requires Python 3.10+, mcp, and a Lean 4 toolchain (elan) for the example project.

pip install mcp pytest
pytest tests/ -v          # one happy path, every rejection path

Wire the server into Claude Code via .mcp.json in your Lean project root:

{
  "mcpServers": {
    "proofrunner": {
      "command": "python",
      "args": ["-m", "harness.mcp_server"],
      "env": {
        "PROOFRUNNER_ROOT": ".",
        "PROOF_FILE_REL": "Example/Bricks.lean",
        "PROOFRUNNER_SPECS": "specs"
      }
    }
  }
}

Then the loop is:

1. Agent calls next_brick and receives the spec (id, target statement, strategy notes, gate, budget).
2. Agent edits the proof file, runs lake build, and generates the axiom check via the scratch-file pattern:

   # AxiomCheck.lean:  import Example.Bricks
   #                   #print axioms myReverse_length
   lake env lean AxiomCheck.lean   # then delete the scratch file
   

3. Agent calls submit_attempt(brick_id, diagnostics_text, print_axioms_text) with the verbatim outputs.
4. On SOFT verified: auto-commit. On HARD verified: you review, then call approve(brick_id, 'Y') to commit or approve(brick_id, 'N') to reject it back to PENDING for revision (the denied attempt still counts against the budget).
5. status shows every brick's lifecycle state at any time.

Demo transcript (abridged)

> next_brick
{ "brick": { "id": "010_myreverse_length", "gate": "SOFT",
  "target": "theorem myReverse_length {α : Type u} (l : List α) : (myReverse l).length = l.length", ... } }

# Agent submits tool JSON instead of the literal #print axioms text:
> submit_attempt("010_myreverse_length", "Build completed successfully.",
                 "{\"axioms\": [\"propext\"]}")
{ "status": "REJECTED",
  "checks": [ ..., { "name": "axiom_whitelist", "passed": false,
    "detail": "print_axioms_text is not the literal '#print axioms' output ..." } ],
  "attempts_remaining": 2 }

# Agent regenerates via the scratch-file pattern and resubmits:
> submit_attempt("010_myreverse_length", "Build completed successfully.",
                 "'myReverse_length' depends on axioms: [propext, Classical.choice, Quot.sound]")
{ "status": "VERIFIED_COMMITTED", "gate": "SOFT", "sha": "..." }

The rejection is the feature. A harness that cannot say no is a rubber stamp with extra steps.

What proofrunner is not

• It does not design your formalization. Deciding what to define and what to prove is the hard part and stays human. proofrunner automates the discharge of bricks a human already approved.
• It is not a proof search tool. It is the referee, not the player. Bring your own agent.
• The automated checks are necessary, not sufficient. The HARD gate exists because there are failure modes (wrong definitions, subtly wrong targets) that no automated check catches.

Repository layout

harness/     verifier.py, dag.py, ledger.py, mcp_server.py
specs/       toy BrickSpecs targeting the example project
example/     minimal Lean 4 project (myReverse + one lemma)
tests/       verifier + scheduling + replay tests
docs/        architecture.md
ledger/      gitignored JSONL resume state (.gitkeep only)

License

MIT. See LICENSE.