sorry2lemma¶
Extract sorry placeholders and unsolved goals at error locations from Lean code and lift them into standalone top-level lemmas.
Python API¶
result = await axle.sorry2lemma(
content=lean_code,
environment="lean-4.26.0",
names=["main_theorem"], # Optional
extract_sorries=True, # Optional
extract_errors=True, # Optional
include_whole_context=True, # Optional
reconstruct_callsite=False, # Optional
verbosity=0, # Optional: 0-2
)
print(result.content)
print(result.lemma_names) # ["main_theorem.sorried", "main_theorem.unsolved"]
CLI¶
Usage: axle sorry2lemma CONTENT [OPTIONS]
# Extract all sorries and errors
axle sorry2lemma theorem.lean --environment lean-4.26.0
# Extract from specific theorems
axle sorry2lemma theorem.lean --names main_proof,helper --environment lean-4.26.0
# Pipeline usage
cat theorem.lean | axle sorry2lemma - --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/sorry2lemma \
-d '{"content": "import Mathlib\ntheorem foo (p q : Prop) : p → q := by\n intro hp\n sorry", "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) |
extract_sorries |
bool |
No | Whether sorries should be lifted into lemmas (default: true) |
extract_errors |
bool |
No | Whether unsolved goals at error locations should be lifted into lemmas (default: true) |
include_whole_context |
bool |
No | Include whole context when extracting (default: true) |
reconstruct_callsite |
bool |
No | Replace sorry with lemma call (default: false) |
verbosity |
int |
No | Pretty-printer verbosity: 0=default, 1=robust, 2=extra robust |
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 sorry2lemma tool with errors, warnings, infos lists |
content |
str |
The transformed Lean code with sorries/errors extracted as lemmas |
lemma_names |
list[str] |
List of names of the newly created lemmas |
timings |
dict |
Timing info: total_ms, parse_ms |
Example Response¶
{
"lean_messages": {
"errors": [],
"warnings": ["-:3:6: warning: declaration uses 'sorry'\n", "-:5:8: warning: declaration uses 'sorry'\n"],
"infos": []
},
"tool_messages": {
"errors": [],
"warnings": [],
"infos": []
},
"content": "import Mathlib\n\nlemma foo.sorried (p q : Prop) (hp : p) : q := sorry\n\ntheorem foo (p q : Prop) : p → q := by\n intro hp\n sorry",
"lemma_names": ["foo.sorried"],
"timings": {
"total_ms": 95,
"parse_ms": 88
}
}
Demo¶
The sorry2lemma tool extracts sorry placeholders and unsolved goals at error locations into standalone lemmas. This is useful for breaking down incomplete proofs into subgoals that can be tackled independently.
extract_sorries and extract_errors¶
You can control which types of goals are extracted:
# Only extract sorries
result = await axle.sorry2lemma(content, environment="lean-4.26.0", extract_errors=False)
# Only extract errors
result = await axle.sorry2lemma(content, environment="lean-4.26.0", extract_sorries=False)
# Extract neither (effectively a no-op)
result = await axle.sorry2lemma(content, environment="lean-4.26.0", extract_sorries=False, extract_errors=False)
include_whole_context, reconstruct_callsite, verbosity¶
Refer to the have2lemma documentation for a detailed description and examples of these fields. sorry2lemma handles them in mostly the same way.
Multiple goals: When a single sorry applies to multiple goals (e.g., after <;>), the tool generates multiple lemmas and combines them with first: