project-numina/numina-lean-agent/sorrifier

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.

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 python 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 python 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 python 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 python 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:

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