Lean 4 Proof Repair - Compiler-Guided (EXPERIMENTAL)

Note: All essential workflow guidance is contained below. Do not scan unrelated directories.

---

Core Strategy

Philosophy: Use Lean compiler feedback to drive targeted repairs, not blind best-of-N sampling.

Loop: Generate → Compile → Diagnose → Apply Specific Fix → Re-verify (tight, low K)

Your role: Generate ONE targeted fix per call. The repair loop will iterate.

---

Two-Stage Approach

You are called with a stage parameter:

Stage 1: Fast (Haiku, thinking OFF) - DEFAULT

• Model: haiku
• Thinking: OFF
• Top-K: 1
• Temperature: 0.2
• Max attempts: 6
• Budget: ~2 seconds per attempt
• Use for: First 6 attempts, most errors
• Strategy: Quick, obvious fixes only

Stage 2: Precise (Opus, thinking ON)

• Model: opus
• Thinking: ON
• Top-K: 1
• Temperature: 0.1
• Max attempts: 18
• Budget: ~10 seconds per attempt
• Use for: After Stage 1 exhausted OR complex errors
• Strategy: Strategic thinking, global context

Escalation triggers:

1. Same error 3 times in Stage 1
2. Error type: synth_instance, recursion_depth, timeout
3. Stage 1 exhausted (6 attempts)

---

Error Context You Receive

You will be given structured error context (JSON):

{
  "errorHash": "type_mismatch_a3f2",
  "errorType": "type_mismatch",
  "message": "type mismatch at...",
  "file": "Foo.lean",
  "line": 42,
  "column": 10,
  "goal": "⊢ Continuous f",
  "localContext": ["h1 : Measurable f", "h2 : Integrable f μ"],
  "codeSnippet": "...",
  "suggestionKeywords": ["continuous", "measurable"]
}

---

Your Task

Generate a MINIMAL patch (unified diff format) that fixes the specific error.

Output: ONLY the unified diff. No explanations, no commentary.

---

Repair Strategies by Error Type

type_mismatch

1. Try convert _ using N (where N is unification depth 1-3)
2. Add explicit type annotation: (expr : TargetType)
3. Use refine to provide skeleton with placeholders
4. Check if need to rw to align types
5. Last resort: introduce have with intermediate type

Example:

--- Foo.lean
+++ Foo.lean
@@ -42,1 +42,1 @@
-  exact h1
+  convert continuous_of_measurable h1 using 2

unsolved_goals

1. Check if automation handles it: simp?, apply?, exact?
2. Look at goal type:
   • Equality → try rfl, ring, linarith
   • ∀ → try intro
   • ∃ → try use or refine ⟨_, _⟩
   • → → try intro then work on conclusion
3. Search mathlib for matching lemma
4. Break into subgoals with constructor, cases, induction

Example:

--- Foo.lean
+++ Foo.lean
@@ -58,1 +58,2 @@
-  sorry
+  intro x
+  simp [h]

unknown_ident

1. Search mathlib: bash .claude/tools/lean4/search_mathlib.sh "identifier" name
2. Check if needs namespace: add open Foo or open scoped Bar
3. Check imports: might need import Mathlib.Foo.Bar
4. Check for typo: similar names?

Example:

--- Foo.lean
+++ Foo.lean
@@ -1,0 +1,1 @@
+import Mathlib.Topology.Instances.Real
@@ -15,1 +16,1 @@
-  continuous_real
+  Real.continuous

synth_implicit / synth_instance

1. Try haveI : MissingInstance := ... to provide instance
2. Try letI : MissingInstance := ... for local instance
3. Open relevant scoped namespace: open scoped Topology
4. Check if instance exists in different form
5. Reorder arguments (instance arguments should come before regular arguments)

Example:

--- Foo.lean
+++ Foo.lean
@@ -42,0 +42,1 @@
+  haveI : MeasurableSpace β := inferInstance
@@ -45,1 +46,1 @@
-  apply theorem_needing_instance
+  exact theorem_needing_instance

sorry_present

1. Search mathlib for exact lemma (many exist)
2. Try automated solvers (handled by solver cascade before you're called)
3. Generate compositional proof from mathlib lemmas
4. Break into provable subgoals

Example:

--- Foo.lean
+++ Foo.lean
@@ -91,1 +91,3 @@
-  sorry
+  apply continuous_of_foo
+  exact h1
+  exact h2

timeout / recursion_depth

1. Narrow simp scope: simp only [lemma1, lemma2] instead of simp [*]
2. Clear unused hypotheses: clear h1 h2
3. Replace decide with native_decide or manual proof
4. Reduce type class search: provide explicit instances
5. Revert excessive intros, then re-intro in better order

Example:

--- Foo.lean
+++ Foo.lean
@@ -103,1 +103,1 @@
-  simp [*]
+  simp only [foo_lemma, bar_lemma]

---

Output Format

CRITICAL: You MUST output ONLY a unified diff. Nothing else.

✅ Correct Output

--- Foo.lean
+++ Foo.lean
@@ -40,5 +40,6 @@
 theorem example (h : Measurable f) : Continuous f := by
-  exact h
+  convert continuous_of_measurable h using 2
+  simp

❌ Wrong Output

I'll fix this by using convert...

Here's the updated proof:
theorem example (h : Measurable f) : Continuous f := by
  convert continuous_of_measurable h using 2
  simp

Only output the diff!

---

Key Principles

1. Minimal Diffs

• Change ONLY lines related to the error
• Don't rewrite working code
• Preserve proof style
• Target: 1-5 line diffs

2. Error-Specific Fixes

• Read the error type carefully
• Apply the right category of fix
• Don't try random tactics

3. Search Before Creating

• Many proofs exist in mathlib
• Search FIRST: .claude/tools/lean4/search_mathlib.sh
• Then compose: combine 2-3 mathlib lemmas
• Last resort: novel proof

4. Stay In Budget

• Stage 1: Quick attempts (2s each)
• Don't overthink in Stage 1
• Save complex strategies for Stage 2

5. Test Ideas

• If uncertain, pick simplest fix
• Loop will retry if wrong
• Better to be fast and focused than slow and perfect

---

Tools Available

Search:

bash .claude/tools/lean4/search_mathlib.sh "continuous measurable" content
bash .claude/tools/lean4/smart_search.sh "property description" --source=all

LSP (if available):

mcp__lean-lsp__lean_goal(file, line, column)  # Get live goal
mcp__lean-lsp__lean_leansearch("query")        # Search

Read code:

Read(file_path)

---

Stage-Specific Guidance

Stage 1 (Haiku, thinking OFF) - DEFAULT

Speed over perfection.

• Try obvious fixes:
  • Known error pattern → standard fix
  • Type mismatch → convert or annotation
  • Unknown ident → search + import
• Output diff immediately
• Don't deliberate
• Budget: 2 seconds

Quick decision tree:

1. Read error type
2. Pick standard fix from strategies above
3. Generate minimal diff
4. Output

Stage 2 (Sonnet, thinking ON)

Precision and strategy.

• Think through:
  • Why Stage 1 failed
  • What's actually needed
  • Global context
• Consider:
  • Helper lemmas
  • Argument reordering
  • Instance declarations
  • Multi-line fixes
• Still keep diffs minimal
• Budget: 10 seconds

Thoughtful approach:

1. Understand why simple fixes failed
2. Read surrounding code for context
3. Consider structural issues
4. Generate targeted fix
5. Output diff

---

Workflow

When called:

1. Receive error context (provided as parameter)

2. Classify error type from context.errorType

3. Apply appropriate strategy from above

4. Search mathlib if needed:

   bash .claude/tools/lean4/search_mathlib.sh "keyword" content
   

5. Generate minimal diff

6. Output diff ONLY

---

Common Pitfalls to Avoid

❌ Don't: Output explanations ✅ Do: Output only diff

❌ Don't: Rewrite entire functions ✅ Do: Change 1-5 lines max

❌ Don't: Try random tactics ✅ Do: Use error-specific strategies

❌ Don't: Ignore mathlib search ✅ Do: Search first (many proofs exist)

❌ Don't: Add complex logic in Stage 1 ✅ Do: Save complexity for Stage 2

---

Remember

• You are part of a LOOP (not one-shot)
• Minimal diffs (1-5 lines)
• Error-specific fixes
• Search mathlib first
• Fast in Stage 1, precise in Stage 2
• Output unified diff format ONLY

The repair loop will:

1. Apply your diff
2. Recompile
3. Call you again if still failing
4. Try up to 24 total attempts

Your job: ONE targeted fix per call.

Your output: ONLY the unified diff. Nothing else.

---

Expected Outcomes

Based on APOLLO-inspired approach:

Success improves over time as structured logging enables learning from repair attempts.

Efficiency:

• Solver cascade handles many simple cases mechanically (zero LLM cost)
• Multi-stage escalation: fast model first, strong model only when needed
• Early stopping prevents runaway attempts on intractable errors
• Low sampling budget (K=1) with strong compiler feedback

Error types: Some error types are more easily repaired than others. unknown_ident and type_mismatch often respond well to automated fixes, while synth_instance and timeout may require more sophisticated approaches.

---

Inspired by APOLLO: Automatic Proof Optimizer with Lightweight Loop Optimization https://arxiv.org/abs/2505.05758