Lean 'Fail on sorry' gate enforces zero obligations: all 12 sorrys are self-exempted by '-- TODO'

[avrabe]

Fail on sorry (post-build gate) in proofs.yml is part of the required Lean proof typecheck (lake build) context. It currently permits every sorry in the tree, and reports No sorrys in proofs/Proofs/ — gate green.

Executed

Against origin/main (2b11af9), the gate's own two-stage pipeline:

$ grep -rn -E '^[[:space:]]*sorry[[:space:]]*(--.*)?$' proofs/Proofs/ | wc -l
12
$ grep -rn -E '^[[:space:]]*sorry[[:space:]]*(--.*)?$' proofs/Proofs/ \
    | grep -v -E 'sorry[[:space:]]*--[[:space:]]*TODO' | wc -l
0

All 12:

proofs/Proofs/Network/MinPlus.lean:189,219,260,313        sorry -- TODO(v1.0.0)
proofs/Proofs/Network/MinPlusPwa.lean:100,113,146,183,
                                      204,219,269,295     sorry -- TODO(v1.0.0)

The exclusion removes all 12. The if never fires. The gate has zero obligations and is green.

Why it drifted

The step's own comment (proofs.yml:143-145) says:

Match bare sorry lines (any indent), excluding those with a same-line comment. The five tracked sorrys do not carry a same-line comment; the gate flags all five.

That was true when written. It is false now: every one of the 12 carries -- TODO(v1.0.0). The count went 5 → 12 with no gate reaction — 8 of the new ones arrived in MinPlusPwa.lean (c7b14b7, 2026-05-03).

The exemption is self-service and unbounded. Appending -- TODO to a sorry is sufficient to exempt it, and nothing anywhere records how many exemptions are outstanding.

The regex is also narrower than the hazard

Only a sorry alone on its own line matches. Not checked anywhere in the workflow:

• := by sorry and := sorry (inline)
• admit
• axiom cheat : 7 = 8

lake build does not fail on sorry either — Lean emits a warning, and build-args is empty so there is no -DwarningAsError=true. leanchecker / nanoda are both false, so there is no external kernel re-check. The grep is the whole enforcement.

Compounding: 8 of the 12 live in a file nothing builds

proofs/Proofs/Network/MinPlusPwa.lean (295 lines) is imported by nothing:

$ git grep MinPlusPwa origin/main | grep -v ':proofs/Proofs/Network/MinPlusPwa.lean:'
CHANGELOG.md:27, CHANGELOG.md:59
artifacts/requirements.yaml:1849
crates/spar-network/src/curves.rs:51
docs/research/... (3 hits)

No .lean file references it. proofs/Proofs.lean lists 10 imports and it is not among them. With defaultTargets = ["proofs"] (a lean_exe rooted at Main, which imports Proofs) and Lake's default lean_lib glob (root module only), that file is never elaborated.

The CHANGELOG is honest about this — "filed out-of-tree" — but artifacts/requirements.yaml:1849 cites it as proof scaffolding, and a reader of the requirement has no way to know the file is neither typechecked nor gated.

(Lake target resolution here is reasoned from the lakefile + Lake's documented defaults, not executed — no local Lean toolchain. The import graph was executed.)

Fix

1. Replace the self-service exemption with a checked-in allowlist. proofs/sorry-allowlist.txt with exact file:line:theorem entries; the gate fails if the found set differs from the allowlist in either direction. Growth fails. So does a stale entry — which is what makes it a ratchet rather than a rubber stamp.
2. Widen the pattern to sorry, admit, and axiom in any position, then let the allowlist carry the exceptions.
3. Print the count on the green path. No sorrys is the same string whether the tree is clean or the grep matched nothing for a structural reason. 0 sorrys found, 0 allowlisted, 47 files scanned cannot be produced by a broken scan. (Same lesson as Mutation Testing gate reads a path cargo-mutants never writes — 4 months of vacuous green (210 survivors reported as 0) #381: absence must not render as success.)
4. Wire MinPlusPwa.lean into a build target, or delete it and stop citing it.
5. Fix the now-false comment at proofs.yml:143-145.

Refs #381 (same species), #382.

[avrabe]

Half of this shipped; the half this issue named second did not. Verified at 618b29df during a multi-persona review.

The self-exemption is genuinely fixed — tools/check_lean_sorries.py counts sorry -- TODO and the floor lives in proofs.yml:166 where the proof author does not edit it in the same commit. That was defect (a).

Defect (b) from the issue body — "the regex is also narrower than the hazard… Not checked anywhere in the workflow: := by sorry and := sorry (inline), admit, axiom cheat : 7 = 8" — is untouched. check_lean_sorries.py:75 is the old gate's pattern verbatim, minus only the -- TODO exclusion:

_SORRY = re.compile(r"^[ \t]*sorry[ \t]*(--.*)?$")

Executed against check() with --max-sorries 0:

file contains	exit	gate reports
sorry alone on its line	1	sorries found: 1
theorem cheat : 1 = 2 := by sorry	0	sorries found: 0
theorem cheat : 1 = 2 := sorry	0	sorries found: 0
theorem cheat : 1 = 2 := by\n admit	0	sorries found: 0
axiom cheat : 7 = 8	0	sorries found: 0

So an author can add an unproven theorem — or assert a falsehood outright via axiom — and the declared floor of 12 is unmoved. The self-service exemption was replaced with a narrower one that is just as self-service.

Compounding it, the self-test pins the gap as intended behaviour rather than finding it (check_lean_sorries.py:178-179):

case("`sorryAx` / inline text is not a bare sorry", 0,
     {"A.lean": "def sorryAx := 1\n-- mentions sorry in prose\n"}, 0)

There is no case for := by sorry, admit, or axiom. 8/8 pass.

Two further items from the issue also remain open:

• A count floor is not the two-directional set equality asked for. Discharge one sorry in MinPlus.lean, add one elsewhere: count stays 12, gate green, nothing records the swap.
• Item 4 (MinPlusPwa.lean unimported) is now Lean proof typecheck never compiles MinPlusPwa.lean — 8 theorems and 8 of 12 sorries sit outside the build graph #397. proofs/Proofs.lean lists 10 imports and does not include it, so 8 of the 12 counted sorries live in a file lake build never elaborates. The count is honest about the text and silent about the fact that two thirds of it is not typechecked at all.

Suggested next step: widen _SORRY to cover inline sorry, admit, and bare axiom (excluding legitimate axiom declarations if any exist — worth checking; there appear to be none in-tree), replace case :178 with cases that require each form to count, and re-measure the floor. Expect the number to rise, which is the point.

Keeping this open for defect (b).