simplify_theorems¶

Simplify theorem proofs by removing unnecessary tactics and cleaning up code.

Input Parameters¶

content · str · required · Lean source code

The Lean source code to be processed by this tool.

names · list[str] · Theorem names to process

Optional list of theorem names to process. If not specified, all theorems are processed. Names not found in the code are silently ignored.

indices · list[str] · Theorem indices to process

Optional list of theorem indices to process (0-based). Supports negative indices: -1 is the last theorem, -2 is second-to-last, etc. If not specified, all theorems are processed.

simplifications · list[str] · List of simplifications to apply

If not specified, all simplifications are applied. See below for available simplifications.

ignore_imports · bool · default: False · Ignore import mismatches

Controls import statement handling:

false (default): Validate that imports match the environment. Returns an error if they don't.
true: Ignore the imports in content and use the environment's default imports instead. See the troubleshooting page for more details.

environment · str · required · Lean environment or version

The Lean environment to use for evaluation. Each environment includes a specific Lean version and pre-built dependencies (typically Mathlib).

Available environments: lean-4.28.0, lean-4.27.0, lean-4.26.0, etc.

timeout_seconds · float · default: 120 · Max execution time in seconds

Maximum execution time in seconds. Requests exceeding this limit return a timeout error. Note that end-to-end request latency may exceed this timeout due to queue time and other overhead. Additionally, all non-admin requests are subject to an absolute maximum timeout of 300 seconds (5 minutes).

Output Fields¶

lean_messages · dict · Messages from Lean compiler

Messages from the Lean compiler with errors, warnings, and infos lists. Errors here indicate invalid Lean code (syntax errors, type errors, etc.).

tool_messages · dict · Messages from simplify_theorems tool

Messages from the simplify_theorems tool with errors, warnings, and infos lists. Errors here indicate tool-specific issues (not Lean compilation errors).

content · string · Lean code with simplified theorem proofs

May be shorter and cleaner than input.

timings · dict · Execution timing breakdown

Timing information in milliseconds for various stages of processing.

simplification_stats · dict · Count of each simplification type applied

Maps simplification names to counts (e.g., {"remove_unused_tactics": 3}).

Available Simplifications¶

remove_unused_tactics

Removes tactics that don't contribute to the proof.

In theorem foo : 1 = 1 := by rfl <;> rfl, the second rfl is useless and should be removed.

remove_unused_haves

Removes unused have statements.

theorem foo (a b : Nat) :
    a ≤ a + b := by
  have h : a + 0 ≤ a + b := by
    apply Nat.add_le_add_left ;
    exact Nat.zero_le _
  simp

In the above theorem, h is useless and should be removed.

rename_unused_vars

Cleans up unused variable names.

In theorem triv (arg : ℕ) : True := trivial, the variable arg is useless. We do not remove it, because that would change the signature of the theorem, but we can clean things up a bit by replacing it with an underscore, as in: theorem triv (_ : ℕ) : True := trivial.

Python API¶

# Simplify all theorems with all simplifications
result = await axle.simplify_theorems(content=lean_code, environment="lean-4.28.0")

# Simplify specific theorems
result = await axle.simplify_theorems(
    content=lean_code,
    environment="lean-4.28.0",
    names=["complex_theorem"],
)

# Apply only specific simplifications
result = await axle.simplify_theorems(
    content=lean_code,
    environment="lean-4.28.0",
    simplifications=["remove_unused_tactics"],
)

print(result.content)
print(result.simplification_stats)

CLI¶

Usage: axle simplify-theorems CONTENT [OPTIONS]

# Simplify all theorems
axle simplify-theorems complex.lean --environment lean-4.28.0
# Simplify specific theorems
axle simplify-theorems complex.lean --names main_theorem,helper --environment lean-4.28.0
# Apply only specific simplifications
axle simplify-theorems complex.lean --simplifications remove_unused_tactics --environment lean-4.28.0
# Pipeline usage
cat complex.lean | axle simplify-theorems - --environment lean-4.28.0 | axle check - --environment lean-4.28.0

HTTP API¶

curl -s -X POST https://axle.axiommath.ai/api/v1/simplify_theorems \
    -d '{"content": "import Mathlib\ntheorem foo : 1 = 1 := by rfl <;> rfl", "environment": "lean-4.28.0", "names": ["foo"]}' | jq

Example Response¶

{
  "lean_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "tool_messages": {
    "errors": [],
    "warnings": [],
    "infos": ["simplify_theorems completed in 1 iterations"]
  },
  "content": "import Mathlib\n\ntheorem foo : 1 = 1 := by rfl",
  "timings": {
    "total_ms": 97,
    "parse_ms": 92
  },
  "simplification_stats": {
    "remove_unused_tactics": 1,
    "rename_unused_vars": 0,
    "remove_unused_haves": 0
  }
}