Lean Prove Lemma

---
description: Close one specific sorry with prover + reviewer + AXLE check cycle
argument-hint: <lemma-slug> --proof-repo PATH --project-url URL --port PORT
---

Run the lean_prover role on one focused lemma, audit with the prover-reviewer, and verify with AXLE `check`. Loop until the proof passes both audits or until retry budget exhausts (then escalate).

**Arguments:** `$ARGUMENTS`
- First positional: `<lemma-slug>` — must match a row in the Lemma Status table of `lean_state.md`
- `--proof-repo PATH`, `--project-url URL`, `--port PORT` as usual
- `--max-retries N` — default 5; how many prover-loop iterations before escalating

## Orchestrator latitude

Paths inside `{PROOF_REPO}/lean/` follow the canonical layout from `/lean-formalize-init`. Prompt templates live under `${MATHPIPEPROVER}/prompts/soft/` — substitute the actual MathPipeProver location. Trust `lean_state.md` over literal paths when reality differs.

## Pipeline reference

Read `docs/lean_pipeline.md` before invoking this skill. The per-lemma cycle described there is:

brainstorm (8c) → prove (87 + AXLE) → review (88) → compile → per-theorem verify (8d)

This skill implements that cycle. Multiple lemmas can be in flight in parallel — brainstorm + review + verify are parallel-safe across lemmas (separate browser chats); the prove step is sequential per shared file so Lean proof-editing backends do not clobber each other.

Subagents are allowed here only because this is Lean formalization and the deliverable is Lean/Mathlib/AXLE proof engineering. Do not generalize this to upstream analytical proof roles; those remain Extended Pro browser submissions.

**Smuggling discipline**: do NOT run `8b_lean_smuggling_check` during the prove-review loop. The proof needs room to breathe. Smuggling-check happens AFTER the lemma passes prove+review+compile, bundled with translation+scope in step 11's per-theorem verify (8d).

## Steps

1. **Read state.** Verify the state is consistent with running the prover now (typically `Current phase: proving_lemmas`). Confirm `<lemma-slug>` exists in the Lemma Status table and is not yet `proved`.

1.5. **Brainstorm (8c) — early, before any prover round-trip.**
   For each lemma that requires a non-trivial structural design (e.g., per-class hypothesis structures, refactored data bundles, novel proof routes), run the design brainstorm BEFORE step 2.
   - Render `${MATHPIPEPROVER}/prompts/soft/8c_lean_design_brainstorm_soft.md` with the lemma signature + paper §-reference + any prior structural commitments.
   - Submit to Extended Pro via `/submit-role`.
   - Brainstorm output: concrete data fields (not abstract Props), proof skeleton, axiom asks with paper citations, smuggling traps to avoid.
   - Verdict PROCEED → continue to step 2 with brainstorm context attached.
   - Verdict PROCEED_WITH_CAUTION → continue with explicit warning.
   - Verdict REDESIGN → escalate to user; do not proceed.
   
   Skip brainstorm for trivial lemmas (e.g., AXLE terminal-tactic closures, definitional unpacks). Use judgment.

2. **CHEAP-FIRST: try AXLE terminal tactics before any Pro round-trip.**
   Before spending a 8-20 min Extended Pro pass, try the auto-prover. AXLE's `repair_proofs` lets you stack multiple terminal tactics, so a single call often closes the easy and medium lemmas at no Pro cost.

   ```bash
   mpp axle repair-proofs \
     --in {PROOF_REPO}/lean/main.lean \
     --names <slug> \
     --terminal-tactics "grind,aesop,simp_all,exact?,decide,omega,polyrith,positivity" \
     --repairs "apply_terminal_tactics" \
     --timeout 900 \
     --log-path {PROOF_REPO}/lean/axle_log.jsonl

If it returns a closed proof, splice it into main.lean, re-AXLE-check, and skip to step 7. If it returns "still has sorry" or compile errors, continue to step 3 (Pro).

You can also batch the whole file: drop --names and AXLE will try the tactic stack at every sorry site. Worth doing once early in the phase to harvest the free closures.

3. IN-THREAD: try a focused proof by hand before invoking Pro. Many lemmas are 1-3 line structural unpacks — ⟨field1, field2, ...⟩ for And/Exists, or by congr; funext; exact h ... for definitional equalities of structures.

   Trigger Pro only when (a) AXLE repair didn't close it and (b) you can't see the proof from the English + Lean signature. This is the most common cost saver in practice.

4. Assemble lemma context (for the Pro pass):

   • The lemma's signature (extract from main.lean)
   • Its English statement (from decomposition.md)
   • The dependencies it cites (other lemmas + Mathlib imports + INVENTORY stubs)
   • Any prior AXLE error trace if this is a retry (kept in diagnostics/lean_prover_<slug>_axle_errors_<n>.txt)

5. Render the prompt from ${MATHPIPEPROVER}/prompts/soft/87_lean_prover_soft.md, with the lemma context as {context_bundle}. Save to diagnostics/lean_prover_<slug>_request_<n>.md.

6. Submit + harvest via /submit-role. Save response to diagnostics/lean_prover_<slug>_response_<n>.md. (Parallelize: if you have several lemmas needing Pro, submit several at once in separate chats — the project supports concurrent chats, and harvesting is independent.)

7. Inspect the response control block:

   • status: STUCK → save the obstruction report, do NOT update the file. Report to the user, recommend either re-decomposition or a Mathlib search. Stop.
   • status: IMPORT_REQUEST → the prover wants an import that isn't in the dep-audit table. Surface to the user — they decide whether to expand the dep-audit or have the prover work around it. Stop.
   • status: PROVED → continue.

8. AXLE verification (BEFORE the reviewer). Splice the new proof into main.lean (or build a test file) and run:

   mpp axle check --in /tmp/lemma_test.lean --log-path {PROOF_REPO}/lean/axle_log.jsonl
   

   • Exit 0 → the proof compiles in context. Continue.
   • Exit 2 → save the error trace to `diagnostic