Running least common multiples: distinct values and multiplicities

Will Cook

Long paper

Running least common multiples: distinct values and multiplicities

Erdős #269 By Will Cook July 2026; revised 5 October 2026 Authorship, AI use and citation

PDFOpen the PDF, 73 pages TeXLaTeX source Source on GitHub Problem page

Summary. For the prime set {2,3,5}, a five-map argument proves irrationality of the sum over distinct running LCMs. Two-prime sums reduce to a transcendental Hecke–Mahler value. For the repeated three-prime sum, an equivalent residue criterion leaves an arithmetic condition open. Complete ordinary arguments for general distinct-running-LCM sums and prime-power subseries are retained as remarks awaiting formalisation.

This paper covers distinct-height irrationality, all-rank kernel structure and the repeated-sum tail criteria, preserving the multiplicity distinction and the remaining open residue-window obligation.

It does not establish the validity of claims tagged Lean, which belongs to the cited kernel-checked source, or a solution to Erdős #269, which remains open.

Start here, by the editorial route

In this paper

Dependencies and remaining questions

The table separates the established special cases from the ordinary generalisations awaiting formalisation and the unresolved repeated-sum condition. Exact kernel rank concerns separation of a function; the residue criterion concerns a scalar sum and still needs arithmetic existence for its segments.

Result	Dependency and limit
Running LCMs and intervals of constancy	Prime-power divisibility and unique factorisation. Their geometry alone gives no irrationality statement.
Two-prime values	Earlier factorisation plus the cited external Hecke–Mahler value theorem. The reduction to that theorem is checked in Lean; the theorem itself is a cited input (Section 14).
Distinct values, every $P$	Integrality of the scaled tails, rearranged chains at a return of the logarithmic flow, Kronecker’s theorem and an Euler characteristic count on a two-dimensional subtorus. Ordinary proof checked by a second agent; no Lean proof. It stops for the repeated sums because their scaled tails are unbounded.
Prime-power subseries	The same two-tail comparison with the integer $f_{p}$ and a chain chosen near the origin of the torus; no two-wall lemma. Ordinary proof checked by a second agent; no Lean proof. Says nothing about the whole repeated sum.
Distinct values, blocks	Dyadic blocks, finitely many affine maps with disjoint images, integrality of the scaled tails and the irrationality of $\log p / \log q$ . The theorem for ${2, 3, 5}$ is checked in Lean; the general criterion has an ordinary proof, and Remark 5.8 adds exact finite computations. No statement about the repeated sums.
Arbitrary-order rank	Diagonal rescaling, separate one-dimensional densities and a staircase determinant; checked in Lean.
Tail recurrence	Counting the original multiplicities, normalising by half the boundary running LCM, and convergence; an abstract recurrence would not identify the sum.
Denominator reduction	A finite prefix with cleared denominators and an upper bound for positive integer tails. The first valid index is determined exactly (Proposition 9.4); checked in Lean.
Residue criterion	The actual recurrence, a dominating bound and segment products comparable to $8^{h}$ ; the inequality at arbitrarily late starts remains unproved.
Weighted differences	Exact reindexing and the contributions of the new boundary strips; integer enumeration checks the displayed counterexample to third-difference cancellation.
Finite computations	Direct checks settle only their individual segments. The two large exclusions have published witnesses and exact checkers, and the larger scan a published saved run; none is a theorem input.

None of these results proves irrationality of the repeated sum $R_{P}$ for three or more primes.

The formal two-prime reduction

The source note in Section 12.5 distinguishes ordinary proofs from individual formal associations. For Theorem 1.2, the Lean development verifies the reduction of that theorem to the transcendence of the Hecke–Mahler boundary sum at an irrational $θ \in (0, 1)$ and nonzero algebraic $β, α$ with $| β | < 1$ and $| β | | α |^{θ} < 1$ , which is Theorem 1.1 of Bugeaud and Laurent [15] in the case $ρ = 0$ , due to Loxton and van der Poorten [16]. Lean does not prove that input; the Lean theorem assumes it. The formal development checks the following parts of the reduction: the running least-common-multiple identity, the selection of the single power of $q$ between consecutive powers of $p$ , the factorisation of the repeated sum, the identification of the distinct running values, the telescoping identity, the boundary identity (6) expressing $A$ through the Hecke–Mahler sum, the irrationality of $\log p / \log q$ , and each side condition verified before the value theorem is applied. The two identities expressing $D_{{p, q}}$ and $R_{{p, q}}$ as polynomials in $A$ are unconditional and carry no additional input.

A theorem whose own statement is conditional is formalised exactly as stated. Theorem 1.2 is asserted unconditionally in this record, and its Lean counterpart carries the additional named input described here.

About this paper

Authorship and AI use. Will Cook built and directed the research infrastructure and maintains the public release. He reviewed claims when he could. AI agents did most of the research and drafting. Cook did not independently verify every claim.

Cite and contact. Cite this paper by its title, author and date above, with its PDF; cite the earlier sources it uses for a mathematical result. For software, use the release citation and give the commit used. Contact Will with questions or corrections.

Prefer the manuscript?

PDFOpen the PDF, 73 pages TeXOpen the LaTeX source Problem page

Equations typeset from the exact TeX. Rendered from the LaTeX manuscript source with file fingerprint sha256:27b68b4b0cf24ce2. Its file fingerprint matched the published source record, so the PDF above, the LaTeX, and this page are one manuscript. Redeploying the site regenerates this page from whatever the public repository holds at that moment.