Repository navigation
proof_status Lean scan: 'sorry' in a doc comment, and the domain.file citation form, deny credit to sorry-free theorems #4351
Description
Found while measuring #3141 (receipt: docs/audits/rust-lean-fidelity-PMAT-3141.md on branch GH-3141-lean-gen-drift). Both fail CLOSED (real proofs are denied, nothing false is granted).
insert_domain_theorems(crates/aprender-contracts/src/proof_status.rs) skips any file wherecontent.contains("sorry").Theorems/TensorTranspose/Roundtrip.leanhas no sorry tactic; line 17 is a doc comment: "compiles sorry-free". Its theorems (transpose_shape, roundtrip_preserves_element, shape_transpose_involution, swapIdx_injective) contribute nothing.Theorems.GgufExportSymmetry.Roundtrip(the domain.file form, apr-gguf-export-symmetry-v1.yaml:44) is never registered: the scan insertsTheorems.GgufExportSymmetryandTheorems.Roundtrip, not the dotted pair.
A fix needs a sorry TOKEN match outside -- and /- -/ comments, a registered Theorems.<Domain>.<Stem> form, and a case table (a comment-only sorry must ground; a real sorry and a sorry in a string or a nested comment must not). Neither fix alone flips a contract to L4: grounding is equation-level (27 self-declared, 70/181 grounded). Whether obligation-level lean.theorem citations should also ground is an ONT-2a design question, owned by ONT.
Activity
refactor(pv): split lean_has_sorry's lexer states into helpers — comp…
noahgift commentedon Sep 25, 2026
Implemented on branch
PMAT-4351-lean-sorry-token@ 8b5bf61 (off batch/0.70.0; no PR — repo at the 10-PR cap, for the apr-fold batch). aprender-a2.lean_has_sorry: thesorrytoken outside--and nested/- -/comments. Fails closed: a sorry in a string literal still counts, and EOF inside a comment or string counts. String and char literals are skipped only so"--"/'"'cannot open a fake comment.insert_domain_theoremsregistersTheorems.<Domain>.<Stem>(theapr-gguf-export-symmetry-v1.yaml:44form).Obligation-level
lean.theoremgrounding stays with ONT-2a, as the issue says.fold: #4351 token-level Lean sorry scan + Theorems.<Domain>.<Stem> (a…
fix(pv): split lean_has_sorry into per-lexeme helpers — the #4351 sca…
Merge #4152 serve lint/soundness fixes + #4351 lean_has_sorry complex…
roadmap(GH-4351): entry with measured tests + the substring-scan mutant
audit(GH-4351): quorum 3/3 PASS on eaa2d3b (sonnet-5 x2 + haiku-4-5; …
fix(pv): a doc-comment 'sorry' and the Theorems.<Domain>.<File> form …
fix(pv): a char literal like '"' opened a phantom string that hid a r…
roadmap(GH-4351): entry with measured tests + the substring-scan mutant
audit(GH-4351): quorum 3/3 PASS on eaa2d3b (sonnet-5 x2 + haiku-4-5; …
audit(quorum): GH-4351,PMAT-4380,PMAT-4581 — AGREED 3/3 PASS (sonnet-…
noahgift commentedon Oct 12, 2026
evidence for close: checked at main 6bd89b0: lean_has_sorry in crates/aprender-contracts/src/proof_status.rs grounds the sorry scan, the Theorems.{domain}.{stem} form is registered, and lean_scan_grounds_doc_comment_sorry_and_domain_file_form in proof_status_tests.rs pins both.
noahgift commentedon Oct 14, 2026
Folded into #5308 as a checklist row (TRIAGE-100, 2026-10-14): the open-ticket cap is 100, so this ticket is now tracked on that master and closed as not planned. Nothing is lost: reopen it when its work resumes, and an open PR for it reopens it. Pushed branch:
91/4351-on-r5a,GH-4351-lean-scan-false-negatives.Agent: aprender-clerk
noahgift commentedon Oct 14, 2026
Row moved: #5308 was split into named masters (TRIAGE-100 master naming), so this ticket's checklist row is now on #5333.
Agent: aprender-clerk