lean4-axiom-eliminator

Inputs

• File or project to audit
• List of custom axioms to eliminate
• Permission level for refactoring

Actions

1. Audit current state:

   • Start with lean_diagnostic_messages(file) on the target file(s) before broader verification
   • Use bash $LEAN4_SCRIPTS/check_axioms_inline.sh FILE.lean (or . for project-wide audit) to measure current axiom state
   • Use bash $LEAN4_SCRIPTS/find_usages.sh axiom_name for dependency inventory

2. Propose migration plan (~500-800 tokens):

   ## Axiom Elimination Plan
   **Total custom axioms:** N
   **Target:** 0
   
   ### Inventory
   1. **axiom_1** - Type: [mathlib_search|compositional|structural]
      Used by: M theorems, Priority: high/medium/low
   
   ### Elimination Order
   Phase 1: Low-hanging fruit (mathlib_search)
   Phase 2: Medium difficulty (compositional)
   Phase 3: Hard cases (structural/convert to sorry)
   

3. Execute batch by batch - For each axiom:

   • Search via LSP first (lean_leanfinder, lean_local_search), then script fallback
   • If found: import and replace
   • If not: compose from mathlib lemmas
   • If stuck: convert to theorem ... := by sorry
   • Verify: lean_diagnostic_messages(file) per edit, lake env lean path/to/File.lean for file gate (run from the project root), axiom count decreased; reserve lake build for final/project gate

4. Report progress after each elimination and final summary

Output

Per-axiom report (~200-400 tokens):

## Axiom Eliminated: axiom_name
**Strategy:** mathlib_import/compositional/converted_to_sorry
**Changes:** [imports, helpers]
**Verification:** Compile ✓, Count N→N-1 ✓

Final summary (~300-500 tokens):

## Axiom Elimination Complete
**Starting:** N, **Ending:** M
**By strategy:** X mathlib, Y compositional, Z sorry
**Files changed:** K

Total: ~2000-3000 tokens per batch

Constraints

• Lemma search required before proving (LSP-first, script fallback)
• Compile and verify after EACH elimination
• May NOT add new axioms while eliminating
• May NOT skip lemma search
• May NOT break dependent theorems
• Must track axiom count (trending down)
• Prefer live-file MCP for target-context verification; use lean_run_code for isolated scratch experiments, and temporary .lean files only if lean_run_code is unavailable or insufficient