sorry2lemma¶

Extract sorry placeholders and unsolved goals at error locations from Lean code and lift them into standalone top-level lemmas.

Try this example in the web UI

Input Parameters¶

content · str · required · Lean source code

The Lean source code to be processed by this tool.

names · list[str] · Theorem names to process

Optional list of theorem names to process. If not specified, all theorems are processed. Names not found in the code are silently ignored. When theorems_only is false, these select over all declarations (not just theorems).

indices · list[str] · Theorem indices to process

Optional list of theorem indices to process (0-based). Supports negative indices: -1 is the last theorem, -2 is second-to-last, etc. If not specified, all theorems are processed. When theorems_only is false, indices position over all declarations (not just theorems).

extract_sorries · bool · default: True · Lift sorries into standalone lemmas

If true, sorry placeholders are extracted into standalone lemmas. Defaults to true.

extract_errors · bool · default: True · Lift errors into standalone lemmas

If true, error positions (type mismatches, etc.) are extracted into standalone lemmas. Defaults to true.

include_whole_context · bool · default: True · Include whole context when extracting

If true, lemmas include all context variables. If false, attempts to minimize the context. Defaults to true.

reconstruct_callsite · bool · default: False · Replace sorry with lemma call

If true, the original sorry is replaced with a call to the extracted lemma. Defaults to false.

merge_duplicates · bool · default: False · Merge duplicate extracted lemmas (by definitional equality)

If true, extracted lemmas within the same parent that are definitionally equal — to each other, or to the theorem/lemma they were extracted from — are merged: duplicates collapse into a single lemma that all callsites reference, and a sorry whose goal is defeq to its parent theorem/lemma is dropped rather than lifted into a restatement (e.g. a top-level := sorry / := by sorry). The parent-restatement check applies only to theorem/lemma parents, not def/instance/etc. Defaults to false.

theorems_only · bool · default: True · Process theorems/lemmas only

If true (default), only theorem/lemma declarations are processed. Set to false to process all declaration kinds (def/instance/abbrev/opaque/etc). When false, names and indices select over all declarations rather than just theorems.

verbosity · float · default: 0 · Pretty-printer verbosity level (0-2)

0=default, 1=robust, 2=extra robust. Higher levels produce more explicit type annotations. Use when default output has ambiguity errors.

ignore_imports · bool · default: False · Ignore import mismatches

Controls import statement handling:

false (default): Validate that imports match the environment. Returns an error if they don't.
true: Ignore the imports in content and use the environment's default imports instead. See the troubleshooting page for more details.

environment · str · required · Lean environment or version

The Lean environment to use for evaluation. Each environment includes a specific Lean version and pre-built dependencies (typically Mathlib).

Available environments: lean-4.28.0, lean-4.27.0, lean-4.26.0, etc.

timeout_seconds · float · default: 120 · Max execution time in seconds

Maximum execution time in seconds. Requests exceeding this limit return a timeout error. Note that end-to-end request latency may exceed this timeout due to queue time and other overhead. Additionally, all non-admin requests are subject to an absolute maximum timeout of 900 seconds (15 minutes).

Output Fields¶

lean_messages · dict · Messages from Lean compiler

Messages from the Lean compiler with errors, warnings, and infos lists. Errors here indicate invalid Lean code (syntax errors, type errors, etc.).

tool_messages · dict · Messages from sorry2lemma tool

Messages from the sorry2lemma tool with errors, warnings, and infos lists. Errors here indicate tool-specific issues (not Lean compilation errors).

content · string · Lean code with sorries/errors extracted as lemmas

The code with sorry and error positions lifted to top-level lemmas with their goals as types.

lemma_names · list · Names of newly created lemmas

Names are auto-generated based on the parent theorem and position.

timings · dict · Execution timing breakdown

Timing information in milliseconds for various stages of processing.

Python API¶

result = await axle.sorry2lemma(
    content=lean_code,
    environment="lean-4.28.0",
    names=["main_theorem"],         # Optional
    extract_sorries=True,           # Optional
    extract_errors=True,            # Optional
    include_whole_context=True,     # Optional
    reconstruct_callsite=False,     # Optional
    merge_duplicates=False,         # Optional
    theorems_only=True,             # 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.28.0
# Extract from specific theorems
axle sorry2lemma theorem.lean --names main_proof,helper --environment lean-4.28.0
# Pipeline usage
cat theorem.lean | axle sorry2lemma - --environment lean-4.28.0 | axle check - --environment lean-4.28.0

HTTP API¶

curl -s -X POST https://axle.axiommath.ai/api/v1/sorry2lemma \
    -d '{"content": "import Mathlib\ntheorem foo (p q : Prop) : p → q := by\n  intro hp\n  sorry", "environment": "lean-4.28.0"}' | jq

Example Response¶

{
  "lean_messages": {
    "errors": [],
    "warnings": ["-:3:6-3:11: warning: declaration uses 'sorry'\n", "-:5:8-5:13: 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.28.0", extract_errors=False)

# Only extract errors
result = await axle.sorry2lemma(content, environment="lean-4.28.0", extract_sorries=False)

# Extract neither (effectively a no-op)
result = await axle.sorry2lemma(content, environment="lean-4.28.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:

-- Input
theorem multiple (n : Nat) : 1 = 1 ∧ 2 = 2 := by constructor <;> sorry

-- Output with reconstruct_callsite=true
theorem multiple (n : Nat) : 1 = 1 ∧ 2 = 2 := by constructor <;> (first | exact multiple.sorried n | exact multiple.sorried_1 n)