Updated 11 September 2026.
The annotations are already implemented: Erdős 427, 750 and 1141 name their assumptions with conditional formal_proof … assuming. Credit #4884, #4885 and #4886. The extractor already exposes proof conditions.
| Remaining responsibility |
Delivery |
| Keep conditional proofs distinct from unconditional proof status; preserve primary/variant semantics |
#4828 |
Check proof-link reachability from published formalProofs |
#4828, incorporating former #4749; Lychee handles HTTP |
| Verify an exact submitted target and retain assumptions, revisions and typed outcomes |
#5387 |
| Show provenance and historical applicability without changing maintainer status |
#5388 |
| Correct specific file/commit proof locators |
Independent #4895 |
The earlier proposal to scan linked text for sorry or axiom is withdrawn. Text scanning misses imported assumptions and cannot establish statement equivalence. A reachable link is only a reachability result. Verification uses the qualified tools and typed result; infrastructure errors remain unevaluated, not rejected proofs.
The original August counts were a dated, linked-file-only survey. They are not the current corpus inventory. The #4884 verification account is corrected in #4394 using the board's retained typed invocation-error record.
Keep this issue open until status interpretation is accepted and exact-target verification/evidence is available with the distinctions above. Mathematical assumptions and maintainer acceptance remain separate from toolkit execution.
Updated 11 September 2026.
The annotations are already implemented: Erdős 427, 750 and 1141 name their assumptions with
conditional formal_proof … assuming. Credit #4884, #4885 and #4886. The extractor already exposes proof conditions.formalProofsThe earlier proposal to scan linked text for
sorryoraxiomis withdrawn. Text scanning misses imported assumptions and cannot establish statement equivalence. A reachable link is only a reachability result. Verification uses the qualified tools and typed result; infrastructure errors remain unevaluated, not rejected proofs.The original August counts were a dated, linked-file-only survey. They are not the current corpus inventory. The #4884 verification account is corrected in #4394 using the board's retained typed invocation-error record.
Keep this issue open until status interpretation is accepted and exact-target verification/evidence is available with the distinctions above. Mathematical assumptions and maintainer acceptance remain separate from toolkit execution.