Lean proof agent

Package:

Demo9_lean_proof_agent.zip

Every other demo on this site ends with a check that is really a judgement: a schema someone wrote, a threshold someone chose, a comparison someone implemented. Mathematics has something almost nothing else has — a checker that cannot be wrong and cannot be persuaded. Lean's kernel either accepts a proof term or it does not.

This demo is about what that does not buy you.

The problem this exists for

A mathematician knows the argument runs step 1 → step 2. The model produces step 1 → a → b → c → step 2. It compiles. Lean is satisfied. The mathematician is not: the proof is correct and no longer shows the argument they cared about.

That is not a failure of the prover. Lean's verdict is binary, so a three-line proof and a fifteen-line wander are equally correct to the kernel. Nothing in the objective rewards brevity or your route.

Which means you cannot prompt your way out of it. "Be concise" does not constrain a search process. The fix has to be structural, and it has two halves: take the route decision away from the model, and measure the shape of what comes back.

1. Look at the three proofs

unzip Demo9_lean_proof_agent.zip
cd Demo9_lean_proof_agent
ls lean/Demo/

Skeleton.lean    the route a person chose, with `sorry` holes
Direct.lean      the proof they had in mind        (3 steps)
Detour.lean      a valid proof that wandered      (15 steps)

The skeleton is the important idea:

theorem sum_bound (a b n : Nat) (ha : a ≤ n) (hb : b ≤ n) :
    a + b ≤ 2 * n := by
  have h1 : a + b ≤ n + n := by sorry
  have h2 : n + n = 2 * n := by sorry
  sorry

The have statements are the argument, written by the human. The sorry holes are the work. An agent may fill holes; it may not rewrite the steps around them. Detours can still happen inside a hole — but a hole is small, and the statements on either side of it are fixed.

2. Run the shape checker — no Lean, no model, no tokens

python3 tools/proof_shape.py \
    --proof lean/Demo/Detour.lean \
    --contract contracts/sum_bound.json

The failed check that matters is not the step count:

required_steps_present:
  missing intermediate statement(s): n + n = 2 * n

Detour.lean is a correct proof. Lean accepts it. And the step the mathematician wanted to see is gone. No amount of kernel-checking would tell you that, because it is not a question about correctness.

Note the skeleton row too: it is short, and it is rejected. An unfinished proof is not a short proof — sorry is caught by its own check before length is even considered.

3. Two checkers, two jobs

lake build          exact, semantic      -> is it a proof?
check_proof_shape   heuristic, textual   -> is it THE proof you wanted?

Be clear about the second one: it reads text and counts. It can be fooled by unusual formatting. It is a guide rail you tune, not a guarantee — the guarantee is the kernel, and the two are not interchangeable.

That honesty is the transferable lesson. In the tissue demos, the schema and check_report were the only checks available; there was no oracle underneath them. Here you can see both layers at once, and see that even with a perfect oracle you still had to write the weak, hand-tuned, subjective check yourself to get the answer you actually wanted.

4. The contract

{
  "theorem": "sum_bound",
  "max_steps": 3,
  "max_depth": 0,
  "required_haves": ["a + b ≤ n + n", "n + n = 2 * n"],
  "allowed_tactics": ["have", "exact", "omega", "apply", "intro", "rfl"],
  "forbidden_tactics": ["sorry", "admit", "native_decide"]
}

This is the mathematician's intent, in a form a script can check. CLAUDE.md tells the agent not to edit it — loosening a contract to make a check pass is the one move that defeats the whole exercise.

5. The two subagents

hole-filler     tools: lean_goal, lean_run_code, lean_build
                fills ONE hole. May not touch neighbouring lines.

shape-referee   tools: check_proof_shape
                cannot run Lean at all. Reports the verdict, does not overrule it.

The scoping is the design, exactly as in Demo 7. shape-referee has one tool and no ability to form an opinion about the mathematics; hole-filler can run Lean but is handed one hole at a time, so it cannot negotiate the route.

Prompts to paste are in prompts/:

1. 1_fill_holes.md — close the holes, one at a time
2. 2_check_the_shape.md — is it the proof I asked for?
3. 3_shorten_it.md — the loop below

6. The loop that actually converges

generate -> lake build -> check_proof_shape -> "shorter, still compiling" -> repeat

This is the evaluator–optimiser pattern from Demo 8, and this is the rare setting where it genuinely works. In most domains the evaluator is another model, so "it got better" is an opinion. Here the acceptance test is exact: it still compiles and it is now four steps instead of fifteen is a fact. Iteration converges because the ground truth is free.

7. The app

python3 -m venv .demo_venv && source .demo_venv/bin/activate
pip install -r requirements.txt
./run.sh

Three tabs: the shape check against the contract, a side by side of the skeleton and the candidate, and does it compile? — which disables itself with an explanation if no Lean toolchain is on PATH, since the rest of the app never needed one.

8. What to take back to a non-mathematical project

The uncomfortable conclusion: mathematics gets the oracle, and still needs the hand-written check. If your field has no oracle, you need the hand-written check even more — and you should be honest that it is the only thing standing between you and a confident wrong answer.

9. Answering the original question

"Sometimes I know the proof runs step 1 → step 2, but the AI routes through a → b → c. How should the agent be designed?"

1. Write the skeleton yourself. The model fills holes; it does not choose the route. This is most of the answer and it needs no new technology.
2. Make shape a measured property. A step budget, the have statements that must survive, an allowed toolbox. Now "too long" is a verdict, not a complaint.
3. Let the loop optimise. Because the kernel is exact, "shorter and still compiling" converges.
4. Split the skeleton across workers. Each hole is an independent subproblem with a perfect acceptance test — orchestrator–workers, with failures that localise to "hole 3" rather than "the proof".

And one thing worth not fixing: a detour is sometimes information. If the direct step cannot be closed and a → b → c can, that occasionally means the direct step wants a lemma that does not exist yet. Log those rather than discarding them.