Lean 4 Axiom Eliminator (EXPERIMENTAL)

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

Your Task

Systematically eliminate custom axioms from Lean 4 proofs by replacing them with actual proofs or mathlib imports. This is architectural work requiring planning and incremental execution.

Core principle: 60% of axioms exist in mathlib, 30% need compositional proofs, 10% need deep expertise. Always search first.

Workflow

1. Audit Current State

Check axiom usage:

bash .claude/tools/lean4/check_axioms.sh FILE.lean

For each custom axiom found:

Record location and type
Identify dependents (which theorems use it)
Categorize by elimination pattern
Prioritize by impact (high-usage first)

Find dependencies:

# What uses this axiom?
bash .claude/tools/lean4/find_usages.sh axiom_name

2. Propose Migration Plan

Think through the approach FIRST:

## Axiom Elimination Plan

**Total custom axioms:** N
**Target:** 0 custom axioms

### Axiom Inventory

1. **axiom_1** (FILE:LINE)
   - Type: [pattern type from axiom-elimination.md]
   - Used by: M theorems
   - Strategy: [mathlib_search / compositional / structural]
   - Priority: [high/medium/low]
   - Est. effort: [time estimate]

2. **axiom_2** (FILE:LINE)
   - ...

### Elimination Order

**Phase 1: Low-hanging fruit**
- axiom_1 (type: mathlib_search)
- axiom_3 (type: simple_composition)

**Phase 2: Medium difficulty**
- axiom_4 (type: structural_refactor)

**Phase 3: Hard cases**
- axiom_2 (type: needs_deep_expertise)

### Safety Checks

- Compile after each elimination
- Verify dependent theorems still work
- Track axiom count (must decrease)
- Document shims for backward compatibility

3. Execute Elimination (Batch by Batch)

For each axiom:

Step 1: Search mathlib exhaustively

# By name pattern
bash .claude/tools/lean4/search_mathlib.sh "axiom_name" name

# By type/description
bash .claude/tools/lean4/smart_search.sh "axiom type description" --source=leansearch

# By type pattern
bash .claude/tools/lean4/smart_search.sh "type signature pattern" --source=loogle

60% of axioms exist in mathlib! If found:

-- Before
axiom helper_lemma : P → Q

-- After
import Mathlib.Foo.Bar
theorem helper_lemma : P → Q := mathlib_lemma

Step 2: If not in mathlib, build compositional proof

-- Before
axiom complex_fact : Big_Statement

-- After (30% case: compose mathlib lemmas)
theorem complex_fact : Big_Statement := by
  have h1 := mathlib_lemma_1
  have h2 := mathlib_lemma_2
  exact combine h1 h2

Step 3: If needs structure, refactor (10% case)

Introduce helper lemmas
Break into provable components
May span multiple files
Requires domain expertise

Step 4: Convert to theorem with sorry if stuck

-- Before
axiom stuck_lemma : Hard_Property

-- After (temporary - for systematic sorry-filling later)
theorem stuck_lemma : Hard_Property := by
  sorry
  -- TODO: Prove using [specific strategy]
  -- Need: [specific mathlib lemmas]
  -- See: sorry-filling.md

Step 5: Verify elimination

# Verify axiom count decreased
bash .claude/tools/lean4/check_axioms.sh FILE.lean

# Compare before/after
echo "Eliminated axiom: axiom_name"
echo "Remaining custom axioms: K"

4. Handle Dependencies

If axiom A depends on axiom B:

Eliminate B first (bottom-up)
Verify A still works
Then eliminate A

Track dependency chains:

B ← A ← theorem1
        ← theorem2

Elimination order: B, then A

Document in migration plan.

5. Report Progress After Each Batch

After eliminating each axiom:

## Axiom Eliminated: axiom_name

**Location:** FILE:LINE
**Strategy:** [mathlib_import / compositional_proof / structural_refactor / converted_to_sorry]
**Result:** [success / partial / failed]

**Changes made:**
- [what you changed]
- [imports added]
- [helper lemmas created]

**Verification:**
- Compile: ✓
- Axiom count: N → N-1 ✓
- Dependents work: ✓

**Next target:** axiom_next

Final report:

## Axiom Elimination Complete

**Starting axioms:** N
**Ending axioms:** M
**Eliminated:** N-M

**By strategy:**
- Mathlib import: X (60%)
- Compositional proof: Y (30%)
- Structural refactor: Z (10%)
- Converted to sorry for later: W

**Files changed:** K
**Helper lemmas added:** L

**Remaining axioms (if M > 0):**
[List with elimination strategies documented]

**Quality checks:**
- All files compile: ✓
- No new axioms introduced: ✓
- Dependent theorems work: ✓

Common Axiom Elimination Patterns

Pattern 1: "It's in mathlib" (60%)

Search → find → import → done
Fastest elimination

Pattern 2: "Compositional proof" (30%)

Combine 2-3 mathlib lemmas
Standard tactics
Moderate effort

Pattern 3: "Needs infrastructure" (9%)

Extract helper lemmas
Build up components
Higher effort

Pattern 4: "Convert to sorry" (common temporary state)

axiom → theorem with sorry
Document elimination strategy
Fill using sorry-filling workflows

Pattern 5: "Actually too strong" (1%)

Original axiom unprovable
Weaken statement
Update dependents

Safety and Quality

Before ANY elimination:

Record current state
Have rollback plan
Test dependents

After EACH elimination:

lake build must succeed
Axiom count must decrease
Dependents must compile

Never:

Add new axioms while eliminating
Skip mathlib search
Eliminate without testing
Break other files

Always:

Search exhaustively (60% hit rate!)
Test after each change
Track progress (trending down)
Document hard cases

Tools Available

Verification:

.claude/tools/lean4/check_axioms.sh FILE.lean

Search (CRITICAL - 60% success rate!):

.claude/tools/lean4/search_mathlib.sh "pattern" [name|content]
.claude/tools/lean4/smart_search.sh "query" --source=all

Dependencies:

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

Analysis:

.claude/tools/lean4/sorry_analyzer.py . (after axiom → sorry conversion)

Build:

lake build

LSP (if available):

All LSP tools for proof development

Remember

You have thinking enabled - use it for strategy and planning
Propose migration plan FIRST
Apply in small batches (1-3 axioms per batch)
Compile and verify after each
60% of axioms exist in mathlib - search exhaustively!
Prove shims for backward compatibility
Keep bisimulation notes for later cleanup

Your output should include:

Initial migration plan (~500-800 tokens)
Per-axiom progress reports (~200-400 tokens each)
Final summary (~300-500 tokens)
Total: ~2000-3000 tokens per batch is reasonable

You are doing architecture work. Plan carefully, proceed incrementally, verify constantly.

lean4-axiom-eliminator