theorem2sorry

Strip proofs from theorems, replacing them with sorry.

Python API

# Convert all theorems
result = await axle.theorem2sorry(content=lean_code, environment="lean-4.26.0")

# Convert specific theorems by name
result = await axle.theorem2sorry(
    content=lean_code,
    environment="lean-4.26.0",
    names=["foo"],
)

# Convert by index (supports negative indices)
result = await axle.theorem2sorry(
    content=lean_code,
    environment="lean-4.26.0",
    indices=[0, -1],  # first and last
)

CLI

Usage: axle theorem2sorry CONTENT [OPTIONS]

# Convert all theorems to sorry
axle theorem2sorry solution.lean -o problem.lean --environment lean-4.26.0
# Convert specific theorems by name
axle theorem2sorry solution.lean --names main_theorem,helper --environment lean-4.26.0
# Pipeline usage
cat solution.lean | axle theorem2sorry - --names main_theorem --environment lean-4.26.0 > problem.lean

HTTP API

# Convert specific theorems by name
curl -s -X POST http://10.1.10.100:8989/v1/axle/theorem2sorry \
    -d '{"content": "import Mathlib\ntheorem left_as_exercise : 1 = 1 := rfl\ntheorem the_tricky_one : 2 = 2 := rfl", "environment": "lean-4.26.0", "names": ["left_as_exercise"]}' | jq

# Convert all theorems
curl -s -X POST http://10.1.10.100:8989/v1/axle/theorem2sorry \
    -d '{"content": "import Mathlib\ntheorem left_as_exercise : 1 = 1 := rfl\ntheorem the_tricky_one : 2 = 2 := rfl", "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 convert to sorry
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, converts all theorems.

Output Fields

Name	Type	Description
lean_messages	dict	Messages from Lean compiler with errors, warnings, infos lists
tool_messages	dict	Messages from theorem2sorry tool with errors, warnings, infos lists
content	str	The Lean code with theorem bodies replaced with 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 left_as_exercise : 1 = 1 := sorry\n\ntheorem the_tricky_one : 2 = 2 := rfl",
  "timings": {
    "total_ms": 97,
    "parse_ms": 92
  }
}