Section 10, paragraph 4Author review of the paper–Lean correspondence is distinct from manual inspection of every proof
Informal interpretation Motivation, interpretation or scope; not a formal claim.
1 Paper text
The author’s review of the formalisation focused on the interface between the paper and Lean: whether the formal definitions, hypotheses and conclusions express the intended mathematical claims. The author did not manually inspect every theorem or lemma declaration or every line of Lean source. Mechanical checking verifies the formal proofs relative to their definitions and stated hypotheses; it does not independently certify the correspondence with the prose, the suitability of the modelling assumptions, or the experimental results.
Generated from paper_jmlr.tex, lines 1293–1293.
2 Explain this
There are two distinct checks: whether Lean accepts a proof of a formal statement, and whether that statement correctly expresses the intended paper claim. The author reports reviewing the second interface without manually reading every helper proof. The linked statements, definitions and source allow readers to examine both levels.
3 How this is formalised
The reported development contains 1,588 theorem/lemma declarations and 24,493 lines across 38 Lean modules, including auxiliary results. A successful build checks formal proofs relative to definitions and explicit hypotheses; it does not discharge an external hypothesis, validate experimental data, or prove that an English paraphrase is faithful. See Section 10 and the coverage record for the boundaries. The new disclosure does not change any Lean source.
| Paper anchor | sec:development-p4 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 10, paragraph 4 |
| Claim | Author review of the paper–Lean correspondence is distinct from manual inspection of every proof |
| Coverage category | Informal interpretation |
| Statement source | paper_jmlr.tex lines 1293–1293; SHA-256 of the normalised block source a2e1e1836ed74897… |
| Explanations | explain/c-author-verification-scope, formal/c-author-verification-scope |
| Build evidence | fresh isolated rebuild, audit report |
4 Lean statement and source
No Lean statement corresponds to this claim. This is interpretation or motivation, not a formal mathematical claim.
Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).