Proof assumptions: status interpretation and exact-target evidence

Updated 11 September 2026.

The annotations are already implemented: Erdős [427](https://github.com/google-deepmind/formal-conjectures/blob/2a0126f6ec4132a0acf3b9562cb2c1f4cfa4041c/FormalConjectures/ErdosProblems/427.lean), [750](https://github.com/google-deepmind/formal-conjectures/blob/2a0126f6ec4132a0acf3b9562cb2c1f4cfa4041c/FormalConjectures/ErdosProblems/750.lean) and [1141](https://github.com/google-deepmind/formal-conjectures/blob/2a0126f6ec4132a0acf3b9562cb2c1f4cfa4041c/FormalConjectures/ErdosProblems/1141.lean) 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.