/lean4

Axiom Elimination Reference

Quick reference for systematically eliminating custom axioms from Lean 4 proofs.

Standard vs Custom Axioms

Standard mathlib axioms (ACCEPTABLE):

• Classical.choice (axiom of choice)
• propext (propositional extensionality)
• quot.sound / Quot.sound (quotient soundness)

Custom axioms (MUST ELIMINATE):

• Any axiom declarations in your code
• Dependencies on unproven theorems

Verification

Check axiom usage:

lean4-skills-check-axioms-inline FILE.lean
lean4-skills-check-axioms-inline .          # scan entire project

For individual theorems:

lake env lean --run <<EOF
#print axioms theoremName
EOF

Using the Axiom Check Script

Always prefer the script over manual checks:

lean4-skills-check-axioms-inline path/to/file.lean
lean4-skills-check-axioms-inline src/   # scan directory recursively

The script handles namespace inference and filters standard axioms automatically.

Why use the script:

• Automatically detects the namespace from the file
• Filters out standard mathlib axioms (propext, quot.sound, Classical.choice)
• Provides clear reporting of non-standard axiom usage
• Handles cleanup of temporary modifications

Limitations:

• Private/protected/local declarations cannot be checked (they're not exported)
• Captures top-level (column-0) declarations only; recognized keywords: theorem|lemma|def|instance|abbrev|example|structure|class|inductive|axiom|constant, optionally prefixed by noncomputable, unsafe, partial, or nonrec. Indented declarations and unicode-identifier decls are not matched.
• Nested, sibling, and dotted namespace blocks ARE tracked correctly (via a scope stack); section blocks handled without leaking into the qualified name
• Any file whose decls all fall in the unmatched classes is surfaced as UNVERIFIED (run exits 1); the previous silent-pass failure mode is gone
• Declarations with access modifiers will show warnings (not errors)

If you must check manually:

namespace MyNamespace
#print axioms myDeclaration
end MyNamespace

Note: Private declarations will still fail with unknownIdentifier - this is expected.

DO NOT create manual axiom-checking files like /tmp/check_axioms.lean:

• The script is more reliable and handles edge cases
• Manual files often miss namespace context
• Manual files need cleanup afterward

Elimination Workflow

Phase 1: Audit Current State

1. Run axiom checker on all files
2. List all custom axioms with locations
3. Identify dependencies (which theorems use which axioms)
4. Prioritize by impact (eliminate high-usage axioms first)

Phase 2: Document Elimination Plan

For each axiom, document:

axiom helper_theorem : P
-- TODO: Eliminate axiom
-- Strategy: [search pattern OR proof technique]
-- Required lemmas: [mathlib lemmas needed]
-- Difficulty: [easy/medium/hard]
-- Priority: [high/medium/low - based on usage count]
-- Est. time: [time estimate]

Phase 3: Search Mathlib Exhaustively

60% of axioms already exist as theorems in mathlib!

Search by name:

lean4-skills-search-mathlib "axiom_name_pattern" name

Search by type/description:

lean4-skills-smart-search "property description" --source=leansearch

Search by type pattern:

lean4-skills-smart-search "type signature pattern" --source=loogle

Phase 4: Eliminate Axioms

Five common patterns:

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

• Search finds existing theorem
• Replace axiom with theorem and import
• Replace body with := mathlib_lemma

Pattern 2: "Compositional proof" (30%)

• Combine 2-3 existing mathlib lemmas
• Prove using standard tactics
• Replace axiom with actual proof

Pattern 3: "Needs domain expertise" (9%)

• Break into smaller lemmas
• Prove components using mathlib
• Combine for final result

Pattern 4: "Actually false" (1%)

• Original axiom too strong
• Weaken to provable version
• Update dependent theorems

Pattern 5: "Placeholder for sorry" (common during development)

• Convert axiom to theorem with sorry
• Fill using sorry-filling workflow
• See sorry-filling.md

Elimination Strategies by Type

Simple Lemmas

-- Before
axiom simple_fact : A → B

-- After (search mathlib)
import Mathlib.Data.Foo
theorem simple_fact : A → B := mathlib_existing_lemma

Compositional Proofs

-- Before
axiom complex_fact : Big_Statement

-- After (prove from components)
theorem complex_fact : Big_Statement := by
  have h1 := mathlib_lemma_1
  have h2 := mathlib_lemma_2
  exact combine h1 h2

Structural Refactors

-- Before
axiom infrastructure : Property

-- After (add structure)
-- 1. Introduce helper lemmas
private lemma helper1 : SubProperty := by ...
private lemma helper2 : AnotherSubProperty := by ...

-- 2. Combine for main result
theorem infrastructure : Property := by
  apply helper1
  exact helper2

Handling Dependencies

If axiom A depends on axiom B:

1. Eliminate B first (bottom-up approach)
2. Document dependency chain
3. Verify elimination doesn't break A
4. Then eliminate A

Dependency tracking:

# Find what uses an axiom
lean4-skills-find-usages axiom_name

Progress Tracking

After each elimination:

# Verify axiom count decreased
lean4-skills-check-axioms-inline FILE.lean

# Compare before/after
echo "Before: N custom axioms"
echo "After: M custom axioms"
echo "Eliminated: $((N - M))"

Expected elimination rate:

• Easy axioms: 2-3 per hour
• Medium axioms: 1-2 per day
• Hard axioms: 2-5 days each

Migration Plan Template

For large axiom elimination work:

## Axiom Elimination Plan

Total custom axioms: N
Target: 0 custom axioms

### Phase 1: Low-hanging fruit (Est: X days)
- [ ] axiom_1 (type: mathlib_search)
- [ ] axiom_2 (type: simple_composition)
- [ ] axiom_3 (type: mathlib_search)

### Phase 2: Medium difficulty (Est: Y days)
- [ ] axiom_4 (type: structural_refactor)
- [ ] axiom_5 (type: domain_expertise)

### Phase 3: Hard cases (Est: Z days)
- [ ] axiom_6 (type: needs_deep_refactor)

Estimated total: X+Y+Z days

Common Pitfalls

❌ Don't:

• Add new axioms while eliminating old ones
• Skip mathlib search (60% hit rate!)
• Eliminate without testing dependents
• Give up after first search failure
• Use stronger axiom to replace weaker one

✅ Do:

• Search thoroughly (multiple strategies)
• Test with lake build after each elimination
• Track progress (axiom count trending down)
• Document hard cases for future work
• Prove shims for backward compatibility

When to Keep Axioms

Rare acceptable cases (WITH user approval):

1. Foundational axioms for new domain (e.g., new mathematical structure)
2. Interface with external systems (FFI, oracles)
3. Temporary scaffolding with CLEAR timeline

Requires:

• Explicit user approval
• Documented elimination plan
• Timeline for removal
• Not acceptable for mathlib contributions

Integration with Subagents

axiom-eliminator agent can:

• Search mathlib exhaustively for each axiom
• Try multiple proof strategies
• Generate elimination patches
• Track progress across batch

Use for:

• Projects with 10+ axioms
• Systematic cleanup work
• When you need to focus on other tasks

Keep human for:

• Novel mathematical insights
• Design decisions
• Hard cases needing creativity

Output Expectations

Agent output expectations:

• Outline plan FIRST (bullet points)
• Show search results
• Propose elimination strategy
• Apply in small batches
• Report progress after each batch
• Total output: ~2000-3000 tokens per axiom