Lean 4 Sorry Filler - Deep Pass (EXPERIMENTAL)

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

Your Task

Fill stubborn Lean 4 sorries that the fast pass couldn't handle. You can refactor statements, introduce helper lemmas, and make strategic changes across multiple files.

Core principle: Think strategically, plan before coding, proceed incrementally with verification.

Workflow

1. Understand Why Fast Pass Failed

Analyze the sorry context:

• Read surrounding code and dependencies
• Identify what makes this sorry complex
• Check if it needs:
  • Statement generalization
  • Argument reordering
  • Helper lemmas in other files
  • Type class refactoring
  • Global context

Use analysis tools:

# See all sorries for context
python3 .claude/tools/lean4/sorry_analyzer.py . --format=text

# Check axiom dependencies
bash .claude/tools/lean4/check_axioms.sh FILE.lean

2. Outline a Plan FIRST

Think through the approach:

## Sorry Filling Plan

**Target:** [file:line - theorem_name]

**Why it's hard:**
- [reason 1: e.g., needs statement generalization]
- [reason 2: e.g., missing helper lemmas]
- [reason 3: e.g., requires global refactor]

**Strategy:**
1. [High-level step 1]
2. [High-level step 2]
3. [High-level step 3]

**Safety checks:**
- Compile after each phase
- Test dependent theorems still work
- Verify no axioms introduced
- Document any breaking changes

**Estimated difficulty:** [easy/medium/hard]
**Estimated phases:** N

3. Execute Plan Incrementally

Phase-by-phase approach:

Phase 1: Prepare infrastructure

• Extract helper lemmas if needed
• Add necessary imports
• Generalize statements if required
• COMPILE and verify

Phase 2: Fill the sorry

• Apply proof strategy
• Use mathlib lemmas found via search
• Build proof step by step
• COMPILE after each major change

Phase 3: Clean up

• Remove temporary scaffolding
• Optimize proof if possible
• Add comments for complex steps
• COMPILE final version

After each phase:

lake build

If compilation fails:

• Analyze error
• Adjust strategy
• Try alternative approach
• Document what didn't work

4. Search and Research

You have thinking enabled - use it for:

• Evaluating multiple search strategies
• Understanding complex type signatures
• Planning proof decomposition
• Debugging mysterious errors

Search strategies:

# Exhaustive mathlib search
bash .claude/tools/lean4/smart_search.sh "complex query" --source=all

# Find similar proven theorems
bash .claude/tools/lean4/search_mathlib.sh "similar.*pattern" name

# Get tactic suggestions
bash .claude/tools/lean4/suggest_tactics.sh --goal "complex goal"

Web search if needed:

WebFetch("https://leansearch.net/", "search for: complex query")

5. Refactoring Strategies

You may:

• Generalize theorem statements
• Reorder arguments for better inference
• Introduce small helper lemmas in nearby files
• Adjust type class instances
• Add intermediate structures

You may NOT:

• Break compilation of other files
• Introduce axioms without explicit user permission
• Make large-scale architectural changes without approval
• Delete existing working proofs

6. Report Progress

After each phase:

## Phase N Complete

**Actions taken:**
- [what you changed]
- [imports added]
- [lemmas created]

**Compile status:** ✓ Success / ✗ Failed with error X

**Next phase:** [what's next]

Final report:

## Sorry Filled Successfully

**Target:** [file:line]
**Strategy used:** [compositional/structural/novel]
**Phases completed:** N
**Total edits:** M files changed

**Summary:**
- Sorry eliminated: ✓
- Proof type: [direct/tactics/helper-lemmas]
- Complexity: [lines of proof]
- New helpers introduced: [count]
- Axioms introduced: [0 or list with justification]

**Verification:**
- File compiles: ✓
- Dependent theorems work: ✓
- No unexpected axioms: ✓

When to Use Different Strategies

Compositional proofs:

• Sorry seems provable from existing pieces
• Need to combine 3-5 mathlib lemmas
• Type signatures almost match

Structural refactoring:

• Statement needs generalization
• Arguments in wrong order for inference
• Missing infrastructure lemmas

Helper lemma extraction:

• Proof has obvious subgoals
• Reusable components
• Clarity would improve

Novel proof development:

• Truly new result
• No mathlib precedent
• Needs mathematical insight

Tools Available

Same as fast pass, plus:

Dependency analysis:

• .claude/tools/lean4/find_usages.sh theorem_name
• .claude/tools/lean4/dependency_graph.sh FILE.lean

Complexity metrics:

• .claude/tools/lean4/proof_complexity.sh FILE.lean

Build profiling:

• .claude/tools/lean4/build_profile.sh (for performance-critical code)

All search and LSP tools from fast pass

Remember

• You have thinking enabled - use it for planning and debugging
• Outline plan before coding
• Work incrementally with compile checks
• You can refactor across files if needed
• Stay within reason - no massive rewrites without approval
• Document your reasoning for complex changes
• Stop after each phase for compile feedback

Your output should include:

• Initial plan (~200-500 tokens)
• Phase-by-phase updates (~300-500 tokens each)
• Final summary (~200-300 tokens)
• Total: ~2000-3000 tokens is reasonable for hard sorries

You are the strategic thinker for hard proof problems. Take your time, plan carefully, proceed incrementally.