repair_proofs

Attempt to repair broken theorem proofs.

Available Repairs

• remove_extraneous_tactics - Remove tactics after the proof is complete
• apply_terminal_tactics - Try terminal tactics in place of sorries
• replace_unsafe_tactics - Replace unsafe tactics with safer alternatives

Python API

# Repair all theorems with all repairs
result = await axle.repair_proofs(content=broken_code, environment="lean-4.26.0")

# Repair specific theorems
result = await axle.repair_proofs(
    content=broken_code,
    environment="lean-4.26.0",
    names=["broken_theorem"],
)

# Apply only specific repairs
result = await axle.repair_proofs(
    content=broken_code,
    environment="lean-4.26.0",
    repairs=["remove_extraneous_tactics"],
)

# Use custom terminal tactics
result = await axle.repair_proofs(
    content=broken_code,
    environment="lean-4.26.0",
    repairs=["apply_terminal_tactics"],
    terminal_tactics=["aesop", "simp", "rfl"],
)

print(result.content)
print(result.repair_stats)

CLI

Usage: axle repair-proofs CONTENT [OPTIONS]

# Repair all theorems
axle repair-proofs broken.lean --environment lean-4.26.0
# Repair specific theorems
axle repair-proofs broken.lean --names main_theorem,helper --environment lean-4.26.0
# Apply only specific repairs
axle repair-proofs broken.lean --repairs remove_extraneous_tactics --environment lean-4.26.0
# Pipeline usage
cat broken.lean | axle repair-proofs - --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/repair_proofs \
    -d '{"content": "import Mathlib\ntheorem foo : 1 = 1 := by\n  rfl\n  simp\n  omega", "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 repair
indices	list[int]	No	List of theorem indices (0-based, negative allowed)
repairs	list[str]	No	List of repairs to apply (default: all)
terminal_tactics	list[str]	No	Tactics to try when apply_terminal_tactics repair is applied (default: ["grind"])
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, repairs all theorems.

Output Fields

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

Example Response

{
  "lean_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "tool_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "content": "import Mathlib\n\ntheorem foo : 1 = 1 := by\n  rfl",
  "timings": {
    "total_ms": 102,
    "parse_ms": 95
  },
  "repair_stats": {
    "remove_extraneous_tactics": 2,
    "apply_terminal_tactics": 0,
    "replace_unsafe_tactics": 0
  }
}

Demo

Supported Features

remove_extraneous_tactics

Removing Tactics After Proof Completion

When a proof is already complete but has extra tactics afterward, this repair removes the extraneous tactics.

Example:

theorem extra_tactics : 1 = 1 := by
  rfl
  simp  -- This tactic is never reached
  omega

After repair:

theorem extra_tactics : 1 = 1 := by
  rfl

apply_terminal_tactics

Applying Terminal Tactics to Complete Proofs

In theorem foo : 1 = 1 := by sorry, the proof is incomplete. This repair attempts to apply terminal tactics to complete the proof. The tactics to try can be customized via the terminal_tactics parameter (default: ["grind"]).

Example:

theorem simple_eq : 1 + 1 = 2 := by
  sorry

After repair:

theorem simple_eq : 1 + 1 = 2 := by
  grind

replace_unsafe_tactics

Replacing Unsafe Tactics with Safe Counterparts

Some tactics like native_decide use native code execution which can be unsafe. This repair replaces them with safer alternatives.

Example:

theorem check_prime : Nat.Prime 7 := by
  native_decide

After repair:

theorem check_prime : Nat.Prime 7 := by
  decide +kernel

Known Limitations

• The repair tool does not guarantee that repaired proofs will be semantically correct or complete
• Some repairs may introduce new errors or conflicts
• Complex proofs with multiple goals may require manual intervention
• The tool works best on simple, localized proof issues