simplify_theorems

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

Available Simplifications

• remove_unused_tactics - Remove tactics that don't contribute to the proof
• rename_unused_vars - Clean up unused variable names
• remove_unused_haves - Remove unused have statements

Python API

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

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

# Apply only specific simplifications
result = await axle.simplify_theorems(
    content=lean_code,
    environment="lean-4.26.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.26.0
# Simplify specific theorems
axle simplify-theorems complex.lean --names main_theorem,helper --environment lean-4.26.0
# Apply only specific simplifications
axle simplify-theorems complex.lean --simplifications remove_unused_tactics --environment lean-4.26.0
# Pipeline usage
cat complex.lean | axle simplify-theorems - --environment lean-4.26.0 | axle check - --environment lean-4.26.0

HTTP API

curl -s -X POST http://10.1.10.100:8989/v1/axle/simplify_theorems \
    -d '{"content": "import Mathlib\ntheorem foo : 1 = 1 := by rfl <;> rfl", "environment": "lean-4.26.0", "names": ["foo"]}' | jq

Input Parameters

Name	Type	Required	Description
content	str	Yes	A string of Lean code
environment	str	Yes	Environment to use (e.g., "lean-4.26.0", "lean-4.25.1")
names	list[str]	No	List of theorem names to simplify
indices	list[int]	No	List of theorem indices (0-based, negative allowed)
simplifications	list[str]	No	List of simplifications to apply (default: all)
ignore_imports	bool	No	If true, ignore import statement mismatches and use the environment's default imports. If false, raise an error on mismatch. Default: false
timeout_seconds	float	No	Maximum execution time (default: 120)

Note: Specify only one of names or indices. If neither specified, simplifies all theorems.

Output Fields

Name	Type	Description
lean_messages	dict	Messages from Lean compiler with errors, warnings, infos lists
tool_messages	dict	Messages from simplify_theorems tool with errors, warnings, infos lists
content	str	The Lean code with simplified theorem bodies
simplification_stats	dict[str, int]	Count of each simplification applied
timings	dict	Timing info: total_ms, parse_ms

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
  }
}

Demo

Supported Features

remove_unused_tactics

Unused/Unreachable Tactics

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

Unused Try Block

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

In the above theorem, the try (rfl) block is useless and should be removed.

remove_unused_haves

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.

Disabled Features

rename_unused_vars

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.

simplify_have_exact

theorem h₁ : (5 : ℝ) ≤ Real.sqrt 26 := by
  have h : 5 ≤ Real.sqrt 26 := by apply Real.le_sqrt_of_sq_le ; norm_num
  exact h

In h₁, the have statement, followed by exact is redundant. The goal can just be proved directly:

theorem h₁ : (5 : ℝ) ≤ Real.sqrt 26 := by
  apply Real.le_sqrt_of_sq_le ; norm_num

However, this causes problems with indentation and formatting that cannot be easily fixed, so this has been disabled for now.

remove_unnecessary_seq_focus

theorem h₁ : (5 : ℝ) ≤ Real.sqrt 26 := by
  apply Real.le_sqrt_of_sq_le <;>
  norm_num

In h₁, the <;> sequence is bad style, and should be removed or replaced with ;. However, in the following example, even though the linter generates the same warning, it is in fact unsound to replace <;> with ;.

theorem ref : 1 = 1 ∨ False := by
  (try left <;>
    try rfl)