A Repository-Based System for Research and Publication

Stored records and derived views

Files store the research state: Lean and manuscript arguments, selected claims and obligations, evidence, entered returns and decisions. Indexes, coordinates and status summaries derive from them. Freshness checks detect disagreement; builders regenerate views. Neither adopts a claim. The architecture guide identifies each view’s source, where repairs belong.

The coverage ledger follows a labelled paper occurrence, identified by location and statement digest, and lists its registered Lean supports and evidence status. A stronger formal result needs an authored relation note bound to both statements. The passage ledger records explanatory text, cited spans, evidence class and rationale. The first asks what supports the statement; the second exposes the explanation’s sources for review. Neither generates prose from a proof.

Finding the relevant work

A problem collection retains proofs, counterexamples, exact experiments, corrected references and failed approaches, so later work can inspect them before choosing another route. Four views provide entry points without requiring a full Lean build (Figure 2).

A declaration is a named Lean definition, theorem or lemma. The declaration index locates it; the dependency index follows the declarations used by selected results. The interpretation graph adds authored accounts of declarations and their connections. The claim registry selects assertions for public reporting and records their status and remaining obligations.

A reader can start from a claim, locate its declarations, follow the recorded dependencies and request the source lines relevant to a question. Declaration locations cover the inventory; dependency edges are exact for selected starts. Interpretations are selective and largely contextual, not records of individual proof review. Lookup locates source without recording execution. A Lean check requires a focused build and inspection of its result.

Operations on the records

The entry points below act on the same repository records. They support a research iteration; their order of use is chosen by the researcher or agent.

A separate self-audit, systems_paper_evidence.py, checks this systems manuscript’s text and cited source bindings. These are implemented interfaces, not reports that every operation has been executed successfully.

An optional proof session illustrates the boundary between producing evidence and adopting a result. It stores notes, exact Lean inputs, process-derived receipts and a closing outcome. Its claim command requires an accepted probe and appends a session claim; it does not alter the reviewed public claim registry. The journal separately checks the sequence and hash chain of entered returns and dispositions. Later work can therefore inspect recorded inputs and decisions without the original conversation.

Responsibilities and adoption

A researcher chooses the question and the evidence needed to answer it. An agent can inspect files, run tools and prepare a change under the public instructions; a contributor can also send an ordinary argument or explanation without a clone or an agent. The maintainer reviews scope, attribution and unresolved obligations before adoption. These are responsibilities, not necessarily different people or agents: contributor and reviewer may coincide. The agent quickstart and contribution guide describe setup and review.

An iteration retrieves relevant work, investigates a question and returns an argument, experiment, correction or manuscript change with its evidence and limits. Review can adopt, revise, defer or reject the proposal. Accepted changes update the authored records; builders regenerate dependent views and release checks test consistency. Structured returns explicitly entered into the journal retain their dispositions. Ordinary issues and pull requests can reach review without a journal session (Section 6).

Permissions and tasks

An integrating agent may change the live checkout; an advisory agent returns a proposal against supplied sources. The repository calls these permissions Type A and Type B.

Permission to edit does not determine the task. Either assignment can concern research, proof or claim audit, literature and attribution, or exposition.

The expected product differs: a candidate argument, a source-located finding, an attribution proposal or a revised manuscript. Each needs the corresponding review.

Exposition preserves established hypotheses, conclusions and evidence status. A suspected mathematical defect is returned for a separate audit or research assignment.

From frozen inputs to an accepted revision

The writer first identifies the result, its antecedents, the difficult explanatory step and the unresolved questions, with source locations.

Selection remains an authorial decision; the manuscript checker tests source consistency and declared rules.

The exchange freezes selected manuscripts, required inputs, coverage records and audit rules under a manifest of their file digests. Writer and integrating reviewer then work from identifiable starting bytes, including any selected uncommitted changes.

An advisory model may work from that packet; a tool-enabled agent may prepare a proposal in a checkout. The packet identifies editable manuscript paths and read-only evidence and tools. Both routes return proposed changes for the same review of mathematical scope, wording and credit.

This figure is drawn in the PDF.

The return checker verifies packet identity and permitted paths, accounts for statement changes, and checks retained labels, citation keys and bibliography entries. It audits the proposed manuscript in a temporary copy of the frozen sources, leaving the live repository unchanged.

It neither applies changes nor executes returned programs. A declared statement change remains an explicit review obligation.

The reviewer then checks the whole statement, its hypotheses and implication directions against all registered supports. An ordinary argument keeps its actual evidence class wherever formalisation is incomplete.

After acceptance, the integrating reviewer edits the owning sources and updates affected evidence bindings. For an assembled companion, the authored sections are edited before rebuilding the flat paper. Integration then regenerates evidence and navigation and includes inspection of the compiled pages, figures and proof links.

Retaining improvements

A reusable writing lesson is a separate proposal, with an example and limits. Adopting it requires a reviewed change to the writing contract.

The packet and audit stages in Figure 5 are implemented by short_paper_writer.py and paper_refinement.py. A return can change the paper without changing the rules for later writers. Accepted lessons revise documents and instructions, not model weights; the procedure itself measures neither reader benefit nor autonomous discovery.

Inventory and formal-support status

The frozen inventory contains 689 paper occurrences, of which 640 have exact or specialising Lean support; 23 depend on a named input and 26 have no recorded Lean support. Of the 640 exact-or-specialising occurrences, 616 are recorded as compared and 24 as queued. These are occurrence counts, not counts of distinct theorems or independently reviewed proofs. Exact support matches the printed statement; specialising support yields it by specialization. Named-input entries retain an additional assumed result. An entry without Lean support may have an ordinary proof; neither of these last two groups is counted as fully covered.

Historical false-edit trial

The historical publication-evidence record reports that nine of the ten deliberately false edits were rejected and one escaped. The edits were authored by the checker’s author, the original run logs were not retained, and the other nine edits were not rerun against the extended checklist. The edits were applied separately, with the baseline restored between trials. The escaped edit changed a description of an unresolved step from “does not supply'' to “completes'', and the publication checks accepted it.

The follow-up tested the intact baseline and only the escaped edit against an added check. It supplies no post-repair ten-of-ten result. In that recorded follow-up, the post-repair witness accepts the current README and rejects a test copy containing the false clause. The trial uses one corpus and the checker’s own selection of errors, with no manual-review control or ordinary continuous-integration comparator. The study locates a coverage boundary. Its nine rejections do not estimate how reliable the checker is.

Local integration and unperformed reader evaluation

On 23 September 2026, a maintainer-operated agent accepted one architecture handoff into a local integration history after focused checks of return routing and architecture packaging. The contributor and reviewer were the same agent. The receipt records no public pull request, human review or independent outside clone replay.

A proposed reader study would hold the mathematical task fixed and compare an ordinary repository, an information-equivalent static briefing and the navigation tools. It would measure understanding and severe errors alongside preparation, use, review and repair costs, retaining missing returns, timeouts and disagreements. No independent writing comparison, blind grading run or cold-reader experiment is reported, so there is no comparative reader result. The records above document inventory, a checker failure and one local integration; general reliability, reader understanding and mathematical transfer remain unmeasured.

Prove2Me.

We use its published version 2, dated 31 August 2026; the first version appeared on 28 August 2026 [31]. Its basic unit is an immutable theorem statement, stored separately from the proofs submitted for it. A proof is checked against the target type in a pinned verification environment. A proof-sketch derives a target using imported theorem statements, some of which may remain open. Contributors can prove those children separately; the target becomes verified when the required children are verified. Immutability makes those local proofs composable without changing their targets [31].

Human review is part of Prove2Me's design. A mission fixes a human-audited core of goals, definitions and milestones; each milestone pairs a source statement with its attested canonical formalisation. For read-back, an independent agent receives the Lean declaration and dependent definitions without the original source; a human compares its mathematical rendering with that source. Natural-language accounts accompany statements and proofs, statement descriptions support library search, and imports give contributors reuse credit. The discussion record also includes a disproved statement followed by a corrected replacement [31]. Explanation, reuse, correction and shared agent work are therefore established parts of this comparison.

For correspondence with a source, the closest analogue is Prove2Me's milestone: both designs identify the mathematical statement whose formalisation is being reviewed. Our coverage record follows a particular paper occurrence and can list several overlapping formal supports, with a relation note explaining their connection to the printed claim. It is not a proof-sketch: listing those supports does not compose proof terms or discharge open lemmas. A separate passage record binds the explanation to sources and rationale, while entered contribution records retain revision decisions and role credit. The focus here is the consistency and review of these publication records across revisions. This difference of focus establishes neither priority for persistent research records nor a measured advantage over Prove2Me.

Polymath, BOINC and GIMPS supply precedents for small mathematical contributions and donated compute [99][97][98], while the Carleson blueprint shows formalisation organised into publicly claimable tasks [87].

The regeneration tools address the familiar build-system problem of keeping derived outputs consistent with their inputs [48]. They run an explicit ordered list of builders and then check the resulting views; this is not a general incremental scheduler. Source bindings and the journal add provenance for assertions and entered returns at particular revisions. Together these mechanisms make dependencies and changes available for inspection. Their effect on research efficiency and semantic correctness needs separate evaluation.

Read a result and follow its sources

The reading guide routes readers through one problem or across the papers, including Reading Eight Erdős Problems Together [17]. Read a result’s short paper, then follow its argument, attribution and formal-support references. Agents can use agent instructions and the workbench’s optional proof sessions. Corrections follow the contribution guide and credit policy.

Inspect the records and rerun document checks

The experiment record contains the ten-edit matrix and limited follow-up in Section 4. The publication-check specification identifies required checks. These structured files trace evidence; they do not replace the paper’s explanation.

From a complete public checkout, run:

python3 scripts/systems_paper_evidence.py
python3 scripts/build_systems_paper_counts.py

The first checks passage-to-source links and content hashes; the second compares the generated inventory with its records. Success establishes agreement, not the correctness of an explanation.

For proof replay, the Lean entry file and CI workflow identify build entry points. The claim register lists curated assertions; release checks cover wider publication requirements. Use the result’s recorded revisions and environment.

A writing packet contains manuscripts, selected records and inspection tools, but no Lean tree. It supports document checks, not a full Lean, Comparator or release rerun.

Locate the formal supports of the worked example

For the weighted criterion in Appendix B, the paper-to-Lean coverage record identifies two formal supports: a weighted criterion and a version whose conclusion explicitly covers every infinite subset. Figure 7 shows the recorded links. The exact declaration names are provided for readers locating them in Lean.¹ These entries support the stated conclusion; they do not assert line-by-line agreement between the ordinary proof and the Lean proofs.

The recorded Comparator runs are the first comparison run and the second comparison run. Comparator checks a formal result against a separately stated challenge. These records concern the specified formal statements, not the historical attribution or the correctness of this paper’s explanation.

The reciprocal-summability criterion attributed to Erdős in Appendix B has its own formal proof, also recorded in the second comparison run.²

Both runs are recorded as compared. Palomar entries are prepared, not submitted; comparison does not establish registry acceptance.

This figure is drawn in the PDF.

Interpret the recorded inventory

The recorded inventory counts occurrences of paper statements, rather than distinct new theorems. Its 689 entries comprise 498 with exact-or-stronger formal support, 142 obtained by specialising a formal result, 23 linked to a named formal ingredient only, and 26 with no registered Lean support. The last two categories do not certify the whole paper statement.

The contribution journal records 7 rounds and 25 returned contributions at the recorded journal revision.³ Of the rounds, 2 are sealed, meaning no further arrivals are expected. Of the returns, 18 have been admitted for integration and 7 remain unreviewed; admission does not itself record integration. Earlier private-history rounds do not constitute a complete public journal.

Explanatory text is recorded for 139,818 of the 152,386 authored theorem-like declarations (91.8%). Most of these descriptions provide surrounding context. This inventory measures the presence of recorded interpretations, not individual proof review or demonstrated reader understanding.

Identify the version and the earlier design accounts

Repository links in this paper identify fixed file versions, so that a reader can inspect the material cited even if the working repository later changes. Unless a link states otherwise, its revision is 992cf60a27ef; the Comparator runs identify their own inputs. No new Lean or Comparator run was performed for this revision.

For archival identification, the initial unified manuscript was prepared from the frozen packet at ced96e58b337, a local integration commit rather than public main. The 29 September state report lists it under the earlier title Problem-Sized Lean Worlds.

This paper supersedes the two earlier design accounts described below. Cite a mathematical result by the paper and version actually used; cite repository software using its software citation record at the chosen commit or release tag.

From a Cold Clone to a Proof Receipt (August 2026) describes the declaration, dependency, interpretation and claim views and the optional recorded proof session. Its counts and audit figures belong to that snapshot; Section 2 describes the current task entry and inspected implementation.

From Spare Compute to Cumulative Mathematics (September 2026) describes contribution roles, reproduction against the original inputs, subsequent integration and role credit. Section 6 gives the current procedure. The earlier paper’s volunteer-compute services, inexpensive adoption by new laboratories and increased discovery rate remain proposals or unmeasured outcomes. These manuscripts explain the design’s history; they are not additional current specifications.

The question and its antecedents

Begin with the series

An infinite subseries retains the terms whose exponents belong to an infinite set $A$ of positive integers. We call $A$ the support: it specifies which terms are present. To allow other integer bases $b\ge 2$, write

These series converge by comparison with a geometric series. The question concerns their arithmetic value: can an infinite choice of retained terms have a rational sum?

Problem 257 asks whether $X_A(2)$ is irrational for every infinite support $A$. The weighted theorem below gives a sufficient condition on $A$; it does not settle that unrestricted question [2][1].

Erdős proved the all-base irrationality conclusion for pairwise coprime exponents satisfying $\sum _{a\in A}1/a<\mathrm{\infty }$. He also stated that coprimality could be removed, without supplying the details [3]. The Problem 257 paper gives a direct proof of that stated extension, as well as the weighted criterion used here [2].

Duverney and Tachiya provide a methodological antecedent: they choose an arithmetic progression by congruences and use averaging to control the remaining contribution [4]. The Problem 257 paper credits that selection method. Its weighted proof uses an additional average over progression lengths, which recovers a factor needed to sum the error bounds. The sources thus supply a classical criterion, an averaging method and the weighted extension, respectively.

A weighted condition on the retained exponents

The weighted condition gives a smaller contribution to exponents divisible by large powers of a fixed set of primes. For $a=2^{k}m$ with $m$ odd, it replaces the reciprocal weight $1/(2^{k}m)$ by $1/[m(2^{2^k}-1)]$. More generally, for a finite nonempty set $P$ of primes, the $P$-part of $a$ is $h_P(a)=\prod _{p\in P}{p}^{v_p(a)}$, where $v_p(a)$ is the exponent of $p$ in the prime factorisation of $a$. Thus $h_{\{2\}}(2^{k}m)=2^k$.

The weighted-support theorem of the Problem 257 paper states that, if

then $X_B(b)$ is irrational for every integer $b\ge 2$ and every infinite $B\subseteq A$ [2].

The conclusion is hereditary: it applies to every infinite subset of $A$. For a fixed base $b$, write $W_{b,P}(A)$ for the sum in (1) with $2$ replaced by $b$. The fixed-base version assumes $W_{b,P}(A)<\mathrm{\infty }$ and gives the same hereditary conclusion at that base. We prove this version below and recover all integer bases from the base-two hypothesis.

Why the weighted condition reaches further

To see why the weight matters, compare it with the older condition $\sum _{a\in A}1/a<\mathrm{\infty }$. Both are tests on the exponents; neither is needed merely for convergence of $X_A(b)$. The source paper gives

This set is arranged in disjoint layers according to the power $2^k$ dividing an exponent. Within layer $k$, reciprocal summation discounts each odd $m$ by $2^{-k}$; weighted summation discounts it by $(2^{2^k}-1{)}^{-1}$. The second discount is much smaller.

Write $S_r=\sum _{1\le m\le 2^r,m\mathrm{odd}}1/m$ for the sum of odd reciprocals up to $2^r$; layer $k$ uses $r=2^k$. Grouping these integers into intervals $[2^j,2^{j+1})$ gives $r/4\le S_r\le r$ for integers $r\ge 2$.

The reciprocal contribution of each disjoint layer is at least $2^{-k}{S}_{2^k}\ge 1/4$. Its weighted contribution satisfies

so the layer contributions have a convergent geometric majorant in the weighted sum.

Thus $\sum _{a\in A_{\star }}1/a$ diverges, whereas $W_{2,\{2\}}(A_{\star })$ converges. The weighted criterion therefore applies to some supports excluded by the reciprocal-summability condition. This is the source paper’s ordinary calculation, with no separate entry in the paper-to-Lean ledger [2].

The proof by two averages

Fix an integer base $b\ge 2$, an infinite support $A$ and a finite nonempty set $P$ with $W_{b,P}(A)<\mathrm{\infty }$. The proof has two parts. Rationality would force a certain positive remainder to be at least the reciprocal of a fixed denominator. Averaging will make that remainder smaller. The main difficulty is that one average leaves an error bound that cannot be summed using the hypothesis; a second average over powers of two supplies the missing factor.

Counting repeated terms changes the question

A running least common multiple is the least common multiple of the terms seen so far in an increasing sequence. Its value can repeat. For integers with prime factors only $2$, $3$ and $5$, the source paper’s example begins $1,2,6,12,60,60,120,360,360,\dots$ [28]. A reciprocal sum counting every occurrence contains $1/60$ twice; one counting distinct values contains it once.

The Problem 269 record proves a result for distinct running least common multiples. The original question counts them with multiplicity, so the result does not automatically answer it [28].

The same record credits Fan’s earlier public two-prime result despite an independently reported derivation, and separately identifies the relevant Hecke–Mahler series literature [28][29][26][27]. Independent derivation does not remove the obligation to cite prior work.

An explicit description and a stronger antecedent

The Euler totient $\phi (n)$ counts the integers from $1$ to $n$ coprime to $n$. The Problem 249 paper studies its subsequences $\phi (k^{j}n+r)$, where $k\ge 2$ is fixed, $j\ge 0$ and $0\le r<k^j$. For each level $j$, it describes the integer linear relations and gives an explicit basis [13]. Coons’s non-$k$-regularity theorem says that no finite set generates these subsequences over all levels. Martin’s stronger separation theorem already implies the independence needed for the basis; the explicit reductions and integral relations are a different contribution. The direct proof uses the Chinese remainder theorem and Dirichlet’s theorem on primes in arithmetic progressions, following an argument in Yazdani that Yazdani credits to Shallit [14][15][16].

Reorganising a proof, making its consequences explicit and formalising it are distinguishable contributions. None makes an inherited ingredient new.

A construction, its formalisation and the historical question

Problem 1041 concerns connecting roots of a polynomial by short curves in a strict lemniscate: for a complex polynomial $f$, this is the region $|f(z)|<1$. The degree-seven counterexample construction is due to the forum contributor ani [23][21]. The recorded Lean result refutes the exact statement in the Formal Conjectures repository; independent human review of its correspondence with the curve-length wording in the 1958 paper has not been recorded [77][24][22]. The construction, its formalisation and that historical correspondence are separate claims.

Readers inspecting the formal result can follow the counterexample assembly and the Hausdorff-length proofs.⁴

The coverage row records exact-or-stronger Lean support for these statements.

Comparator remains pending for this result, so its recorded Lean support should not be described as a completed formal comparison.

The other seven motivating targets remain unresolved in this work.

A revised statement must retain its scope, attribution and registered supports. Sharpening, merging or moving it requires renewed review of its relation to every support and named input.