lean4-axiom-eliminator

Why this score

This repo hosts 4 subagents, so its 227 stars are split between them (about 57 each) for scoring.

Popularity score: 61/100 from public GitHub signals only. It shows how widely used and maintained this is, not how well it works. Not included yet: the fake-star check. The security scan is shown separately and doesn't change the score. How we rank

What it can use

• ! Run shell commands
• ✓ Edit and write files
• ✓ Read and search files

Tools listed in the file: Read, Grep, Glob, Edit, Bash, lean_goal, lean_local_search, lean_leanfinder, lean_leansearch, lean_loogle, lean_diagnostic_messages, lean_run_code

Model: opus

This agent can act outside your files. Read it before installing, and narrow its tools: line if it needs less.

The agent file

---
name: lean4-axiom-eliminator
description: Remove nonconstructive axioms by refactoring proofs to structure (kernels, measurability, etc.). Use after checking axiom hygiene to systematically eliminate custom axioms.
tools: Read, Grep, Glob, Edit, Bash, lean_goal, lean_local_search, lean_leanfinder, lean_leansearch, lean_loogle, lean_diagnostic_messages, lean_run_code
model: opus
---

## 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):
   ```markdown
   ## 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):
```markdown
## 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):
```markdown
## 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

## Example (Happy Path)

```
## Axiom Elimination Plan
**Total:** 2, **Target:** 0

1. **helper_lemma** - mathlib_search, used by 3 theorems

---

Searching: bash $LEAN4_SCRIPTS/search_mathlib.sh "helper" name
Found: Mathlib.Foo.helper_lemma

## Axiom Eliminated: helper_lemma
**Strategy:** mathlib_import
**Changes:** Added import, replaced axiom with theorem
**Verification:** ✓ Count 2→1
```

## Tools
**LSP-first** (use before scripts; fall back only when LSP is unavailable, rate-limited, or inconclusive after bounded attempts):
```
lean_goal(file, line)
lean_diagnostic_messages(file)
lean_leanfinder("query")
lean_local_search("keyword")
lean_loogle("type pattern")
lean_run_code("code")
# Script fallback:
$LEAN4_SCRIPTS/check_axioms_inline.sh
$LEAN4_SCRIPTS/find_usages.sh
$LEAN4_SCRIPTS/search_mathlib.sh
$LEAN4_SCRIPTS/smart_search.sh
lake build
```

## See Also

- [Extended workflows](../skills/lean4/references/agent-workflows.md#lean4-axiom-eliminator)

Apache-2.0 license, from frenzymath/Archon at commit 3fe261887080.

Security

Scanned Oct 21, 2026 at commit 3fe261887080, with Cisco's open-source skill-scanner.

None of the patterns we list turned up: shell commands, network requests, reading environment variables, downloading and running code, or installing packages.

A scan lists patterns in the code. It can't prove an add-on is harmless, and it can miss things, so read what you install. How we scan

Alternatives

Other makers' add-ons that do the same job, next to this one.