theorem2lemma

Convert between theorem and lemma declaration keywords.

Python API

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

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

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

# Convert to theorem instead
result = await axle.theorem2lemma(
    content=lean_code,
    environment="lean-4.26.0",
    target="theorem",
)

CLI

Usage: axle theorem2lemma CONTENT [OPTIONS]

# Convert all theorems to lemmas
axle theorem2lemma theorems.lean --environment lean-4.26.0
# Convert specific theorems by name
axle theorem2lemma theorems.lean --names foo,bar --environment lean-4.26.0
# Convert to theorem instead
axle theorem2lemma lemmas.lean --target theorem --environment lean-4.26.0
# Convert first and last theorems
axle theorem2lemma theorems.lean --indices 0,-1 --environment lean-4.26.0
# Pipeline usage
cat theorems.lean | axle theorem2lemma - --environment lean-4.26.0 | axle check - --environment lean-4.26.0

HTTP API

# Convert all to lemmas
curl -s -X POST http://10.1.10.100:8989/v1/axle/theorem2lemma \
    -d '{"content": "import Mathlib\ntheorem foo : 1 = 1 := rfl\ntheorem bar : 2 = 2 := rfl", "environment": "lean-4.26.0"}' | jq

# Convert specific theorems by index to theorems
curl -s -X POST http://10.1.10.100:8989/v1/axle/theorem2lemma \
    -d '{"content": "import Mathlib\nlemma foo : 1 = 1 := rfl\nlemma bar : 2 = 2 := rfl", "environment": "lean-4.26.0", "indices": [0], "target": "theorem"}' | 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
indices	list[int]	No	List of theorem indices (0-based, negative allowed)
target	str	No	Target keyword: "lemma" or "theorem" (default: "lemma")
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 (may under-report errors in proof bodies)
tool_messages	dict	Messages from theorem2lemma tool with errors, warnings, infos lists
content	str	The transformed Lean code
timings	dict	Timing info: total_ms, parse_ms

Example Response

{
  "lean_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "tool_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "content": "import Mathlib\n\nlemma foo : 1 = 1 := rfl\n\nlemma bar : 2 = 2 := rfl",
  "timings": {
    "total_ms": 106,
    "parse_ms": 100
  }
}