A Lean 4 Proof Repair Workflow That Stays Reproducible

1. Reproduce before editing

Start from a clean checkout and record the toolchain and dependency revisions. Run the exact build command that exposes the failure. A proof that only fails in one warm editor session is not yet a reproducible defect.

lean --version
lake --version
lake build
git rev-parse HEAD
git status --short

2. Minimize the failing declaration

Copy the failing declaration into a scratch module with only the imports it needs. Remove unrelated definitions until the remaining failure is small enough to explain. If removing an import changes the error, that dependency relationship is part of the bug.

Do not rewrite the theorem statement while minimizing unless the statement itself is suspected. Changing the claim and changing the proof at the same time makes the repair impossible to audit.

3. Read the goal and context

Inspect the local context, the target, and the transparency or reducibility settings that affect unfolding. The right tactic is often less important than noticing that the simplifier cannot see a definition, or that an induction hypothesis has the wrong shape.

• ✓Check whether the goal is definitionally equal to a known lemma.
• ✓Check whether a needed hypothesis was generalized away.
• ✓Check whether the induction motive matches the conclusion.
• ✓Check for typeclass or decidability obligations hidden by notation.

4. Repair in small, checkable steps

Prefer a sequence of small changes that each compile. A common repair pattern is to introduce a local helper lemma, prove its statement independently, then use it to shorten the main proof.

5. Verify outside the editor

Run the project build from a clean process and inspect the diff. Confirm that no axioms or unsafe declarations were introduced, that the theorem statement is unchanged unless explicitly approved, and that the build artifact is tied to the recorded revision.

The final handoff should name the exact command, revision, changed files and unresolved assumptions. That is the difference between a proof repair and a screenshot of a green line.