sorry2lemma

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

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.

• indices · list[int] · 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.

• 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
  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 definitionally equal to its parent theorem/lemma is dropped rather than lifted into a restatement. 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. 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: True · Ignore import mismatches
  Controls import statement handling:

  • true (default): Ignore the imports in content and substitute the environment's default header.
  • false: Process the imports in content exactly as written.

• 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.

• timeout_seconds · float · default: 120 · Max execution time in seconds
  Maximum execution time in seconds. Requests exceeding this limit return a timeout error.

Output Fields

• lean_messages · dict · Messages from Lean compiler
  Messages from the Lean compiler with errors, warnings, and infos lists.

• tool_messages · dict · Messages from sorry2lemma tool
  Messages from the sorry2lemma tool with errors, warnings, and infos lists.

• 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.

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
  }
}

The sorry2lemma tool extracts sorry placeholders and unsolved goals at error locations into standalone lemmas.