sorry in proof 証明中に sorry が残っている

Error message

declaration uses 'sorry'

Lean 4 emits this as a warning, not a hard error, so it is trivial to overlook in a large build. Under the zero-sorry discipline of LeanDFumt and Rei-AIOS, any occurrence is treated as a blocking fault.

Minimal reproduction

-- File: Example.lean
theorem foo : 1 + 1 = 2 := by
  sorry

Build output:

Example.lean:2:2: warning: declaration uses 'sorry'

Why it happens

sorry is Lean's placeholder for an unproven goal. It closes any goal at any type, so the file compiles, but the declared theorem is not actually proved. Downstream code that depends on the theorem will build, and tests that rely on the theorem being true may pass by coincidence — until a real counterexample surfaces.

Fix

Complete the proof with real tactics. For decidable propositions on finite types — the common case in LeanDFumt — by decide or by native_decide suffices:

theorem foo : 1 + 1 = 2 := by decide

-- DFUMT8 examples (require: import LeanDFumt; open LeanDFumt)
example : DFUMT8.and .BOTH .TRUE = .BOTH := by decide
example : DFUMT8.neg .BOTH = .BOTH := by decide

If the goal is genuinely open — i.e. you do not yet know how to prove it — do not leave sorry. Instead:

  1. Mark the file with an -- OPEN: comment describing the missing step.
  2. Exclude the file from the default lakefile.toml target.
  3. Record the goal in the project's open-problem list.

This preserves the invariant that every default-target build is zero-sorry, while still letting exploratory work live in the repo.

Detection: CHECKER_SPEC

v0 primitive (available today — spec §4, Appendix A): Lean emits declaration uses 'sorry' as a warning, not an error, so the file compiles and can even emit VERDICT VALID on stdout. The v0 checker wrapper MUST intercept the sorry warning in Lean's stderr and return UNDECIDED / MISSING_AXIOM with the warning line preserved in detail — MISSING_AXIOM is the reason code that means "a required proof step is not present." This is the single most important v0 discipline for a zero-sorry project: the check belongs at the wrapper, not at the source.

Post-v0 Layer 2 (planned — spec §13): locate_first_error(kind = "sorry") traverses the elaborated declaration tree in source order and returns the position of the first Expr.mvar whose head symbol resolves to sorryAx. If any is found, the file fails the zero-sorry gate regardless of whether Lean itself would only warn. Layer 2 is a thin wrapper over v0 and does not introduce independent decision logic.

See also