From Lean Proofs to Public Claims

What the certificates are for

Erdős Problem 249 asks whether the totient constant $$S=\sum_{n\ge 1}\frac{\varphi(n)}{2^{n}}$$ is  [3], meaning that it is not $a/b$ for any integers $a$ and $b$ with $b\ne 0$. Here $\varphi$ is Euler’s totient function: $\varphi(n)$ counts the integers from $1$ to $n$ sharing no factor greater than $1$ with $n$. The following exact equivalence explains why the certificates matter. Multiplying $S$ by $2^N$ makes its first $N$ terms integral; write $R_N$ for the remaining rescaled tail. Thus $R_N$ differs from $2^N S$ by an integer. Put $D_{N,h}=R_{N+h}-R_N$. It differs from $2^N(2^h-1)S$ by an integer. For $h>0$, the factor $2^N(2^h-1)$ is a nonzero integer, so an integral $D_{N,h}$ would force $S$ to be rational. Conversely, every rational number has an eventually repeating binary expansion, the base-2 analogue of a repeating decimal. Thus some $h>0$ makes $D_{N,h}$ integral for every sufficiently large $N$. Lean checks the exact equivalence: $$S\text{ is irrational}\quad\Longleftrightarrow\quad D_{N,h}\notin\mathbb Z\ \text{ for every $h>0$ and every $N$}.$$ For fixed $h$ and $N$, Lean proves $D_{N,h}\notin\mathbb Z$ exactly when a certificate exists at a finite depth $L$. Its integer calculation approximates $2^L D_{N,h}$ with error at most $r=N+h+L+2$. The certificate checks that the residue modulo $2^L$ lies strictly between $r$ and $2^L-r$, outside both bands compatible with an integral value. The omitted infinite tail is thus accounted for by an explicit bound. The claim record calls this a . We use the shorter word : it proves only that this particular tail difference is not an integer.

The scales of the finite theorem compress this two-parameter requirement to one. The diagonal $H_t=\operatorname{lcm}(1,\dots,t)$ is the least common multiple of $1,\dots,t$: the smallest positive integer divisible by every integer in that list. It is therefore divisible by every candidate period up to $t$. If $S$ were rational, its binary digits would have a period $h_0$ after a position $N_0$. For $t\geq\max(h_0,N_0)$, one has $h_0\mid H_t$ and $H_t\geq N_0$, so rationality would make $D_{H_t,H_t}$ integral; a diagonal certificate rules this out. The development proves the reduction exact: certificates along the diagonal beyond every fixed cutoff are equivalent to the full two-parameter requirement, and therefore, through the chain above, to the irrationality itself. Certificates on a finite list, however long, are not.

Writing $\mathrm{Cert}(t)$ for “a certificate exists at scale $t$”, the two statements then read: $$\begin{align*} \text{checked:}&\ \ \mathrm{Cert}(t)\ \text{for every integer $t\le82$;}\\ \text{open:}&\ \ \text{for every cutoff }T,\ \mathrm{Cert}(t)\ \text{for some }t>T. \end{align*}$$ The boundary between them is a matter of logical form, not of scale. The bound 82, 820, or any other fixed bound stands in the same relation to the open requirement: a larger cutoff still exists. No finite interval implies the second statement without a theorem that produces new witnesses. In particular, no certificate at $t=83$, and no cofinal supply, is claimed. This is the boundary an edit can silently delete.

The formal evidence

The historical module deposits certificates at 28 prime-power breakpoints through $t=64$. Because $H_t$ is constant between breakpoints, its combined theorem already covers every $t\le66$. The later module adds the remaining finite arithmetic and proves : for every $t\le82$, there is a checking depth and a certificate at period and position $H_t$. The claim record names six supporting declarations across the two Lean libraries.

Lean’s is the small trusted program that checks every accepted proof. These finite certificate proofs use decide, which evaluates a finite proposition and supplies a proof term for the kernel . Separately, proves the exact tail-difference, pointwise-certificate, and diagonal equivalences, ending at . The default lake build compiles the libraries rooted at and , including the module that proves the $t\le82$ theorem.

What “coverage” means here

The word needs an object. This project separately tracks which named Lean items exist, where readers can find them, which statements a person has described, and which descriptions were approved for public use. Those are inventory, navigation, interpretation, and public-claim coverage; none implies the next. Lean calls a named theorem or definition a . Indexing every declaration is not understanding every theorem, and understanding every theorem would still not find every sentence that mentions one. Dated inventory counts belong in Appendix ; they are navigation facts, not a result.

The reviewed record

The quoted record entry contains four names specific to this repository. A is the certificate defined in Section . The entry abbreviates least common multiple as “lcm”, so its are the values $H_t$. The are the periods 1 through 8, each handled by one explicit certificate. A is the same calculation at a fixed period, position, and depth, isolated in another Lean file and checked by decide.

Table  shows the substance of the corresponding entry in docs/claims.json, ordered as a reader meets it: what is claimed, where it stops, what remains open, then the supporting machinery. The entry also records an exact source line for each declaration; those coordinates are omitted from the table.

The table records rather than explains the claim. Its public statement, bounded domain, remaining-open link, and status record a human judgement about meaning. Under the proved equivalence, the remaining-open field is essential: without it, the entry no longer separates the finite theorem from an answer to Problem 249. The identifier and source lines instead help software find the entry and may be refreshed when code moves.

No field establishes that the English is faithful to Lean. The maintainer read the final theorem, judged that the wording claims the listed scales and no more, and confirmed that the unbounded requirement remains open. The record stores that judgement, not its justification. Review asks whether wording is faithful; authorisation decides what the project publishes. One maintainer performed both here. A later change to either theorem or wording reopens the review; automatic checks can only preserve the decision that was recorded.

What the checker verifies here

For this claim, scripts/check_release.py verifies a finite list of relationships. Declaration names must remain near their recorded source locations, and all checked Lean source must byte-match the saved revision. The limitation clause must remain on each registered public page, and generated views must equal a fresh rebuild. These tests establish presence, identity, and proximity, not implication. Lean checks the theorem; the release program checks the recorded description around it; a person remains responsible for the claim that the two say the same thing.

Historical exercise.

The structured report in docs/publication_evidence.json identifies a saved Git revision. It says that ten deliberate false edits were applied to a separate copy one at a time and ran the release checker, but not Lean. They covered seven configured relationship kinds, including status, source coordinates, boundary wording, generated-file freshness, and size budgets. The original run logs were not retained; the file is a report, not raw output.

According to that record, nine of the ten edits were rejected. One escaped: the README clause saying that the finite cases the open requirement was changed to say that they it, asserting exactly the missing bridge to Problem 249. Lean was untouched, and the checker passed because the clause was absent from its checklist. The escape shows that a passing checker does not certify all public prose; it gives no detection rate.

Repair and present test.

The repair required the clause and added a deliberately false example, called a in the repository: it crosses a consequential public boundary while leaving every Lean proof intact. The post-repair witness accepts the current README and rejects a test copy containing the false clause. The other nine edits were not rerun against the extended checklist, so there is no post-repair aggregate result.

Later reconstruction.

The executable reconstruction preserves three original targets and uses seven documented replacements. It is a new experiment, not the missing runs.

The evidence marks a coverage boundary, not a reliability score. The edits were authored by the checker’s author; all seven relationship kinds were represented, but five of them by one edit each; and no controlled comparison with disciplined manual review was run. Reader error, ordinary use, and transfer were not measured.

Requiring a clause to be present does not detect a contradictory stronger claim elsewhere on the page. Coverage grows only when a person notices and records a relationship; selected high-risk commitments also have a negative fixture, that is, a deliberately false version which the check must reject. Coverage can also shrink: deleting a registered relationship leaves no rule requiring it, so every remaining check passes. Retiring a commitment therefore deserves the same review as creating one.

The shape of this limit is familiar from Section . A configured checklist, like a finite certificate interval, does not exhaust an open-ended domain. The comparison is only structural: prose has no equivalence theorem and no diagonal compresses it.

Three boundaries the companion papers exposed.

Three later corrections fell outside the checklist for different reasons. A kernel-checked headline in the Problem 249 note had no claim-record entry, so it carried no reviewed public status. A Problem 257 support described as open had been settled in the literature in 2019, outside the repository. A valid parity theorem was presented as a frontier until adjoining one support element was seen to remove the obstruction: the theorem was correct but its advertised significance was not. These are respectively a registration gap, stale external status, and representation-dependent significance. They are incidents, not a rate, and none is detectable by comparing recorded artefacts with one another.

The failures the design addresses.

The checks address accidental disagreement after a sound review. A declaration may move while its recorded line number stays fixed, and a generated view may be stale or hand-edited. A rewrite may remove a required limitation, a status may be upgraded, or the shipped Lean files may cease to be the reviewed ones. A check may also decay until it can no longer fail. In each case, one recorded item disagrees with the others, which a mechanical comparison can detect.

The failures it does not address.

Three failure modes remain outside the design. a paraphrase can strengthen a claim without touching a registered anchor, and a contradiction, misleading emphasis, or new public document can escape for the same reason. Requiring one clause to be present does not require the page to agree with it. a maintainer can alter source, record, and prose together, so every comparison agrees. If the certificate definition were weakened while the record and prose were updated to match, all checks could pass although the public reading of the equivalence was wrong. if the original judgement was wrong, the machinery preserves the mistake. It checks persistence, not the quality of the judgement.

The checked boundary.

Only listed relationships are checked. The repository calls their set its (historically, its “assurance perimeter”); in ordinary terms, this is simply the boundary of the checklist. A recorded commitment inside the boundary triggers an automatic check. Outside it, the checker is silent. The name must not suggest more: choosing what belongs on the checklist remains a human judgement, and a passing check does not make the contents true. This repository gives priority to headline results and to wording whose accidental strengthening would change the project’s public status, as the deleted boundary clause did under the equivalence. If the same claim appears on several pages, the checker sees only the appearances named in the record.

Several narrower limits belong to this implementation rather than to the general pattern. One maintainer performs both review and authorisation; the checker tolerates a theorem name within three lines of its recorded location; some prose checks require exact wording; the exercise used one edit per relationship type; and the original logs were not retained.

What another project could reuse.

The file formats are incidental. The pattern applies whenever a checked formal result sits beside a tempting stronger public statement: finitely many cases beside a statement about all cases; a conditional theorem beside its unproved hypothesis; one implication beside an alleged equivalence; or a theorem under assumptions beside an unconditional headline. What transfers is the reviewed boundary between the exact formal result and its nearest unproved strengthening.

The minimum obligations are concrete. Each selected public claim needs its own wording, named formal evidence, exact source version, scope, assumptions, and explicit stronger non-conclusions. Human mathematical review must be distinguished from automatic consistency checking. Every generated public view needs a named builder. Proof checking and publication checking must be separate and able to fail independently. Every recorded relationship needs a specified mechanical check; selected high-risk boundaries should also have a deliberately false example which that check rejects. Finally, the project must describe its selection as selective rather than complete.

What is not established.

The architecture does not establish a solution to either Erdős problem; that a formal statement is the statement the author intended; that software understood any unregistered prose; that the record is complete; that one maintainer’s review is independent or adequate; or that the design transfers to other projects with its behaviour intact. A large number of passing comparisons measure none of those things. What a passing workflow establishes is narrower: the configured jobs ran on the named revision, Lean accepted the formal proofs, and every configured structural comparison passed. This paper is an architecture note with one bounded case study and three naturalistic incidents, not an empirical evaluation of the design. A credible evaluation would need review records naming reviewer and revision, wrong edits authored by someone other than the checker’s author, and only then a comparison with ordinary review on the same changes. None of those stages exists here, and this paper claims none of them.

Proof blueprints.

A pairs an informal outline with Lean declarations and uses author-supplied links to record which results depend on which earlier results. leanblueprint stores that outline in TeX and its checkdecls command checks only that each named declaration exists [6]; it neither infers the dependency links nor checks that the informal and formal statements agree. LeanArchitect attaches blueprint metadata to Lean source, infers dependencies and unfinished-proof status, and exports synchronised TeX [7]. Text and unformalised nodes remain human responsibilities. Both systems primarily support a formalisation in progress. The claim record here instead starts after a selected proof has been accepted and asks which public wording was reviewed and which stronger conclusion remains open.

Reviewing intended mathematical meaning.

Lean Atlas and EconCSLib ask whether a formalisation expresses its intended source mathematics. Lean Atlas leaves semantic verification to people. Given chosen theorem statements, its Lean Compass selects the project declarations whose meaning can affect them, narrowing what a person must inspect; it assumes Lean’s standard library and the mathematical library Mathlib are semantically correct rather than inspecting them [8]. The authors’ soundness claim is conditional on the semantic correctness of every returned declaration and the trusted base; project-level coverage additionally requires the chosen theorem set to exhaust the intended claims. It does not find every claim occurrence in later public prose. EconCSLib instead has a model write Lean. At statement level, one context-blind model pass translates Lean back to LaTeX and a second compares that translation with the source; a separate holistic audit checks cross-statement drift, and a dashboard records human judgements. At present all model validations run through one Codex agent stack, so errors may correlate. Table 3 lists 865 human-translation review rows across 24 papers; only 10 have saved human review, all in one paper, and two of those are marked uncertain [9]. This paper addresses a later boundary: it starts from accepted Lean proofs and asks how subsequent public wording can remain within a reviewed interpretation of them.

An audit of formal-theorem benchmarks likewise finds that kernel acceptance does not establish fidelity to the intended natural-language problem. Across five benchmarks and 13 released variants, its static checkers produced 4,833 findings, including 398 with machine-checkable certificates of unprovability or vacuity; a separate semantic audit evaluated a curated 92-problem challenge set across six error categories and achieved high recall but low precision, so human adjudication remained necessary [10]. That work concerns incoming benchmark statements; this repository concerns outgoing claims made after a proof. Its program is narrower than semantic verification and still cannot prove that every claim-bearing passage was selected.

Checked documents and traceability.

Isabelle/DOF, a document system built on the Isabelle proof assistant, places formal and informal material in one checked document. Authors define an : document classes with typed fields and rules. They label passages with those classes, and Isabelle’s editor reports rule violations as they edit [11]. The bounded domain and open conclusion in Table  could be typed fields in such an ontology. This repository keeps prose unrestricted and checks a separate record; its checker cannot inspect prose that the record does not name.

Testing the boundary.

CASCADE derives tests and an alternative implementation from the same documentation using language models. It reports a likely inconsistency only when $\mathtt{f2p}>0$ (at least one generated test fails on the original implementation and passes on the generated one) and $\mathtt{p2f}=0$ (no generated test changes in the opposite direction). A person must still confirm the report [12]. Unlike the present checker, it can inspect documentation that was not registered in advance.

Mutation testing deliberately seeds faults and asks whether tests distinguish the altered program from the original [13][14]. The ten false edits in Section  serve that purpose only. They were selected by hand, and nine were not rerun after repair, so they yield neither a post-repair detection rate nor a mutation-adequacy score.

Requirements traceability follows a requirement through development and revision. Gotel and Finkelstein distinguish its production before a requirements specification from its deployment afterwards . The claim record is closer to bounded post- specification traceability: it does not reconstruct exploratory requirement production, changing responsibility, or contributor access. An assurance case is a reasoned argument supported by evidence; Goal Structuring Notation (GSN) is one graphical notation for documenting its claims, evidential references, context, and asserted support relationships [16]. The standard is explicit about the boundary: the notation documents an asserted argument but establishes neither its truth nor that it sufficiently supports the top claim [16]. The claim record resembles those elements but is not an assurance argument: it contains no chain of reasoning asserting that the Lean declarations justify the public wording. It records the approved wording, source, scope, and limits; the justification remains a human judgement.

Dated navigation counts.

At the semantic review’s snapshot, taken before the eight-problem consolidation of 2026-08-02 enlarged the corpus to 153,238 declarations, all 151,761 then-live declarations were inventoried and routed, and all 143,098 author-written theorem-like declarations had an exact node link. Of those, 139,753 (97.7%) participated in authored mathematical interpretations: 3,265 as exact proposition evidence and 136,488 as bounded certificate- or module-family context. The remaining 3,345 were linked only through exact source-module and normalised-signature families, not authored mathematical paraphrases. Every declaration selected for a public claim had an authored route. The command python3 scripts/query_semantic.py coverage derives these volatile navigation counts and checks their references. They do not measure semantic review quality or public-claim completeness.

The reviewed claim record, docs/claims.json, names the saved Git revision of the Lean source, which the release checker requires to match exactly. This paper omits the changing commit identifier so that the claim record is the only place that states it.

Declaration of generative AI use.

Every word of this manuscript was generated by agents based on large language models operating within Will Cook’s private research system for artificial intelligence. The formal proofs and repository software were likewise drafted and revised by the agents through that system under Cook’s direction. Cook set the objectives and acceptance criteria, selected and reviewed the public claims, and approved the published version. Cook assumes responsibility for the accuracy, interpretation, and presentation of the work. Generative systems are production tools, not authors, and supply no independent authority. That boundary is the subject of this paper as well as a condition of it: the checker described in Section  tests recorded relationships a person selected, so passing it does not make generated wording faithful. The author selected, reviewed, and authorised the public claim-to-declaration mappings, and remains responsible for connecting the proofs to public wording.

The paper inventory, , records source and PDF cryptographic hashes and validation commands. The evidence file for Section , , records the protocol, outcomes, and limitations. The reconstruction file, , specifies the ten edits. The script checks that each edit applies once (--verify-operators) and, by default, runs all ten in a copy of the saved evaluation version (--all). For an edit whose exact original target was not preserved, the file names a fixed replacement. The original raw outputs were not retained; the reconstruction does not claim to be them.

The papers build with Tectonic or standard LaTeX via make -C paper. The tracked root PDF is the shipped copy, and the inventory checks its file hash. These identities name artefacts; they do not interpret them.