sorrifier

name	sorrifier
description	Isolates failing proof steps by replacing them with `sorry` and extracting them into standalone lemmas to modularize and decouple complex Lean 4 proofs.

Sorrifier — Proof Isolation Workflow

Structural refactoring workflow for isolating broken proof steps. Replaces failing logic with sorry, extracts it into a standalone lemma, and reconstructs the call site so the main theorem compiles cleanly.

Tools Used

This workflow uses two tools from other skills. All commands go through the logging wrapper.

Tool	Skill	Purpose
uv run --no-project .claude/skills/cli/lean_check.py FILE	verification	Diagnose compilation errors and pinpoint failing lines
uv run --no-project .claude/skills/cli/axle.py sorry2lemma	code-transform	Extract sorry into standalone lemma with --reconstruct-callsite

For full parameter reference, see verification/reference-lean-check.md and code-transform/reference-axle-sorry2lemma.md.

Execution Workflow

Follow these steps sequentially:

Step 1: Diagnose

Run uv run --no-project .claude/skills/cli/lean_check.py FILE to identify failing lines.

• Read lean_messages for entries with severity: "error".

Step 2: Inject sorry

Edit the Lean code: replace the failing tactic/expression with sorry.

• Scope the sorry to the smallest failing block, not the entire theorem.

Step 3: Verify sorrified state

Run uv run --no-project .claude/skills/cli/lean_check.py FILE again.

• Acceptance: zero errors. Warnings about declaration uses 'sorry' are expected.
• If errors persist, adjust sorry placement and repeat.

Step 4: Extract to lemma

Run uv run --no-project .claude/skills/cli/axle.py sorry2lemma with:

• --reconstruct-callsite (required) — replaces sorry with the extracted lemma call
• --names <theorem> — target only the specific theorem
• Omit --no-include-whole-context if local context variables need capturing

Step 5: Final verification

Run uv run --no-project .claude/skills/cli/lean_check.py FILE one last time.

• Acceptance: main theorem compiles by calling the new lemma. Unresolved logic is isolated in the extracted lemma.

Example

Broken state:

import Mathlib.Tactic

theorem sum_of_squares_helper (n : ℕ) : (n + 1)^2 = n^2 + 2*n + 1 := by
  have h1 : (n + 1)^2 = (n + 1) * (n + 1) := by ring
  rw [h1]
  exact magic_solve n  -- error: unknown identifier

After sorrify + extract:

uv run --no-project .claude/skills/cli/axle.py sorry2lemma file.lean --environment lean-4.28.0 --names sum_of_squares_helper --reconstruct-callsite

import Mathlib.Tactic

lemma sum_of_squares_helper_lemma_1 (n : ℕ) (h1 : (n + 1) ^ 2 = (n + 1) * (n + 1)) :
  (n + 1) * (n + 1) = n ^ 2 + 2 * n + 1 := by
  sorry

theorem sum_of_squares_helper (n : ℕ) : (n + 1)^2 = n^2 + 2*n + 1 := by
  have h1 : (n + 1)^2 = (n + 1) * (n + 1) := by ring
  rw [h1]
  exact sum_of_squares_helper_lemma_1 n h1

Best Practices

• Scope narrowly: Sorry the specific subgoal or have statement, not the entire theorem.
• Rename: The tool generates generic names (e.g., lemma_1). Rename to something meaningful.
• Next step: Once extracted, solve the lemma independently using informal_prover or manual proof.