have2sorry

Replace have statements in proofs with sorry. Useful for creating problem templates from solutions while keeping the overall proof structure intact.

Python API

result = await axle.have2sorry(
    content=lean_code,
    environment="lean-4.26.0",
    names=["main_theorem"],  # Optional
)
print(result.content)

CLI

Usage: axle have2sorry CONTENT [OPTIONS]

# Replace all have statements
axle have2sorry theorem.lean --environment lean-4.26.0
# Replace from specific theorems
axle have2sorry theorem.lean --names main_proof,helper --environment lean-4.26.0
# Pipeline usage
cat theorem.lean | axle have2sorry - --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/have2sorry \
    -d '{"content": "import Mathlib\ntheorem foo : 1 = 1 ∧ 2 = 2 := by\n  have h1 : 1 = 1 := by rfl\n  have h2 : 2 = 2 := by rfl\n  exact ⟨h1, h2⟩", "environment": "lean-4.26.0"}' | 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 process
indices	list[int]	No	List of theorem indices (0-based, negative allowed)
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, processes all theorems.

Output Fields

Name	Type	Description
lean_messages	dict	Messages from Lean compiler with errors, warnings, infos lists
tool_messages	dict	Messages from have2sorry tool with errors, warnings, infos lists
content	str	The transformed Lean code with have statements replaced by sorry
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 ∧ 2 = 2 := by\n  have h1 : 1 = 1 := sorry\n  have h2 : 2 = 2 := sorry\n  exact ⟨h1, h2⟩",
  "timings": {
    "total_ms": 95,
    "parse_ms": 88
  }
}