Erdős problem #68

The factorial-denominator series

Is the series $\sum_{n \geq 2} 1 / (n! - 1)$ irrational?

Open Problem on GitHub

Read the short paper PDFOpen the PDF, 9 pages Map of results

The problem

The question

Starting at 2!, the factorials are $2! = 2, 3! = 1 \cdot 2 \cdot 3 = 6, 4! = 24, \dots$ . Subtract 1 and add the reciprocals: $S = 1 + 1 / 5 + 1 / 23 + 1 / 119 + \dots$ . The partial sums approach 1.2534987…. Is that limit irrational, meaning it cannot be written as a fraction of two integers? Every finite partial sum is a fraction; the question concerns the infinite sum.

An example

Through $n = 5$ , the denominators are 1, 5, 23 and 119. Multiplying by $5! = 120$ leaves fractions $120 / 23$ and $120 / 119$ . To make every term an integer, the smallest multiplier is their least common multiple (LCM), $13685 = 5 \cdot 23 \cdot 119$ . But this much larger multiplier also enlarges the remaining tail.

Is $\sum_{n \geq 2} \frac{1}{n! - 1}$ irrational?

Erdős problem #68, as erdosproblems.com/68 states it

The setup in detail

The symbol $\sum_{n \geq 2}$ says: put $n = 2, 3, 4, \dots$ in turn into $1 / (n! - 1)$ and add the results, without end. The factorial $n!$ is the product $1 \cdot 2 \dots n$ , so $2! = 2$ , $3! = 6$ , $4! = 24$ , $5! = 120$ . The sum starts at $n = 2$ because $1! - 1 = 0$ .

An endless sum means the number its partial sums approach. Write $H_{N}$ for the sum of the terms from $n = 2$ to $n = N$ , so $H_{3} = 1 + 1 / 5 = 6 / 5$ . The partial sums increase, and they stay below 1.27. Indeed

(n + 1)! - 1 = (n + 1) (n! - 1) + n,

so each term is less than the one before divided by $n + 1$ . From $1 / 5$ on, each term is less than a quarter of the one before, and

S < 1 + \frac{1}{5} (1 + \frac{1}{4} + \frac{1}{16} + \dots) = 1 + \frac{4}{15} = 1.2666 \dots

So the partial sums settle on one number, $S = 1.2534987 \dots$ .

Irrational means that $S$ cannot be written as $a / q$ with integers $a, q$ and $q \geq 1$ . A proof must rule out every denominator $q = 1, 2, 3, \dots$ , infinitely many of them. Computing digits cannot do that: however many places are computed, some fraction agrees with $S$ in all of them. Each partial sum $H_{N}$ is a fraction; the question concerns the whole infinite sum.

The example in detail

For comparison, $e = 1 + 1 + 1 / 2! + 1 / 3! + \dots$ . Multiplying its terms from $n = 2$ through $n = 5$ by $5! = 120$ gives integers, because each $n!$ with $n \leq 5$ divides 120:

\frac{120}{2!} + \frac{120}{3!} + \frac{120}{4!} + \frac{120}{5!} = 60 + 20 + 5 + 1 = 86.

The partial sums of $S$ , each in lowest terms, are $H_{3} = 6 / 5$ and

H_{4} = \frac{6}{5} + \frac{1}{23} = \frac{6 \cdot 23 + 5}{5 \cdot 23} = \frac{143}{115}, H_{5} = \frac{143}{115} + \frac{1}{119} = \frac{143 \cdot 119 + 115}{115 \cdot 119} = \frac{17132}{13685} .

Multiplying by 120 leaves two terms as fractions:

120 H_{5} = 120 + 24 + \frac{120}{23} + \frac{120}{119} = 150.2257 \dots

Here 23 is a prime larger than 5, and $119 = 7 \cdot 17$ , so neither divides 120. The newest term always fails in this way: a prime dividing both $N!$ and $N! - 1$ would divide their difference, which is 1.

The smallest multiplier that makes $H_{5}$ whole is its denominator 13685. Compare the two multipliers on the tail $S - H_{5} = 0.0016171 \dots$ :

120 \times 0.0016171 \dots = 0.1940 \dots, 13685 \times 0.0016171 \dots = 22.130 \dots

The factorial keeps the tail below 1 and leaves fractions; the common denominator makes every term whole and multiplies the tail past 1.

The crux

The chart tests an irrationality strategy: assuming a rational total, find a multiplier making it and the early terms integers. The multiplied tail must then be an integer; keeping it strictly between 0 and 1 gives a contradiction. Horizontally, $N$ is the last included index; the logarithmic height shows multiplier times remaining tail. Blue uses $e = 1 + 1 + 1 / 2! + 1 / 3! + \dots$ and multiplier $N!$ , keeping below 1. Red uses our sum and its common denominator: it crosses 1 at $N = 4$ and grows. The result below bounds the common denominator’s growth, before cancellation in the summed fraction. Irrationality remains open.

Why the blue curve proves irrationality of e. Suppose $e = a / q$ with integers $a, q$ and $q > 0$ . Choose $N \geq max {q, 2}$ and multiply by $N!$ .

$N! e = N! a / q$ is an integer, since q is a factor of N!.
Every early term $N! / n!$ for $n \leq N$ is an integer; call their sum W.
The multiplied tail is positive, and $N! e - W = \frac{1}{N + 1} + \frac{1}{(N + 1) (N + 2)} + \dots < \frac{1}{N + 1} + \frac{1}{(N + 1)^{2}} + \dots = \frac{1}{N} .$
It is therefore an integer strictly between 0 and 1, a contradiction.

The blue dots plot that multiplied tail. For example, at N=3 it is $6 e - (6 + 6 + 3 + 1) = 0.3096 \dots$ . Both curves use a logarithmic vertical scale: equal rises represent equal multiplication factors, rather than equal additions.

What changes for our sum. Write $H_{N}$ for the sum of the terms through $1 / (N! - 1)$ . The tail $N! (S - H_{N})$ is also small, but $N! H_{N}$ need not be an integer, as the example above shows. Instead use $L_{N} = lcm (2! - 1, \dots, N! - 1)$ , which makes each early term an integer. The red dots plot this multiplier times the remaining tail: about 0.27 at N=3, 1.15 at N=4 and 10³⁰ at N=12. Eventually it grows without bound: consecutive denominators are coprime, so $L_{N} \geq ((N - 1)! - 1) (N! - 1)$ , while the tail exceeds $1 / ((N + 1)! - 1)$ . Their product tends to infinity.

The result below strengthens the common-denominator bound to $\underset{N \to \infty}{lim inf} \log L_{N} / (N^{3 / 2} \log N) \geq 2 \sqrt{2} / 3$ . This concerns the number clearing every individual term, before adding. Cancellation can reduce the denominator after adding: 139 divides $L_{137}$ but not the reduced denominator of $H_{137}$ . No corresponding growth bound for the reduced denominator is proved here.

An exact remaining test. Let $C_{N}$ be the first integer strictly above $N! H_{N}$ . If $S = a / q$ and N is larger than q and 2, then $N! S$ is an integer divisible by N. Since $0 < N! (S - H_{N}) < 1$ , this integer is $C_{N}$ . The long paper proves the converse too: S is rational exactly when N divides $C_{N}$ for every sufficiently large N. At N=5, $C_{5} = 151$ , which 5 does not divide. Among N=3, …, 600, the divisibility holds only at 52 and 591. These finite checks cannot settle the question: what remains is to prove failures at arbitrarily large N.

The common denominator $L_{N}$ is the smallest positive integer divisible by every denominator 2!−1, …, N!−1. Large denominators force it upwards unless they share large factors. The left posts compare 8!−1 and 11!−1: multiplying the first by $990 = 9 \cdot 10 \cdot 11$ puts both below the same ceiling, 11!. The posts fall 990 and 1 below that ceiling. Every shared factor divides their gap, $989 = 23 \cdot 43$ ; the ladder shows 43 steps of 23. Generally, the greatest common divisor of $i! - 1, j! - 1$ is below $N^{j - i}$ when $2 \leq i < j \leq N$ . Measure sizes in powers of N, so multiplication adds heights. The lower-right columns count denominators backwards from N=50. The kth has gaps 1, …, k−1 to later ones; stacked cells add their shared-factor bounds. Each denominator has leading height 50. Red marks what remains above the shared-factor bounds. The first ten columns give total size 500, minus at most 165. These are asymptotic sizes and upper bounds, not measured factors. How many denominators should we use? Set k approximately equal to $α \sqrt{N}$ . On the upper graph, after a common rescaling, the line $α$ is the product's contribution and the curve $α^{3} / 6$ is the shared-factor bound. Their vertical gap is what the LCM must retain. The largest gap is $2 \sqrt{2} / 3$ , at $α = \sqrt{2}$ : the red segment. It gives $\underset{N \to \infty}{lim inf} \log L_{N} / (N^{3 / 2} \log N) \geq 2 \sqrt{2} / 3$ . This bounds the common denominator before cancellation. The summed fraction's reduced denominator may be smaller; irrationality of the infinite sum remains open.

Define $d_{n} = n! - 1$ for $n \geq 2$ and $L_{N} = lcm (d_{2}, \dots, d_{N})$ . Thus $L_{N}$ clears the denominators of the partial sum, whose reduced denominator may be smaller. The greatest common divisor (gcd) measures the shared factor of a pair. For $2 \leq i < j \leq N$ , set $R = j! / i!$ . The identity $R d_{i} - d_{j} = 1 - R$ implies $gcd (d_{i}, d_{j}) ∣ R - 1 < N^{j - i}$ . Multiplication by R aligns the factorial parts so that subtraction leaves only the short gap.

Lemma 3.1 gives product ≤ LCM times the product of all pairwise gcds; prime by prime, the largest exponent is retained by the LCM and the smaller exponents are covered by those pairwise factors. Applying this to the terminal block yields $\log L_{N} \geq \sum_{n = N - k + 1}^{N} \log d_{n} - (\binom{k + 1}{3}) \log N$ , because $\sum_{h = 1}^{k - 1} h (k - h) = (\binom{k + 1}{3})$ counts the total index gap over all pairs. This is an exact inequality, not a subtraction of measured common factors.

With $k = ⌊ α \sqrt{N} ⌋$ , the selected indices satisfy $n / N \to 1$ uniformly. The elementary factorial bounds in Theorem 3.4 therefore make the normalised log-product tend to $α$ , while the allowance tends to $α^{3} / 6$ . Consequently $\underset{N \to \infty}{lim inf} \log L_{N} / (N^{3 / 2} \log N) \geq α - α^{3} / 6$ . Its maximum over $α > 0$ is $2 \sqrt{2} / 3$ , attained at $α = \sqrt{2}$ .

The $N = 50$ bars use leading height $N$ , not actual log-factorial heights; the cubic is an upper allowance, not observed gcd growth. Only vertical differences in the graph represent the bound. The theorem gives neither a bound for the reduced denominator nor irrationality of the series.

Results and open questions

#68. Put $S = \sum_{n \geq 2} 1 / (n! - 1)$ and $L_{N} = {lcm}_{2 \leq n \leq N} (n! - 1)$ . Any rational $S = a / q$ with $q > 0$ satisfies the two incomparable exclusions $q ∤ 299999!$ and $q \geq 2^{39990} > 10^{12038}$ . The first is a factorial divisibility constraint from a fresh exact GMP carry census through $m = 300000$ together with a Lean consumer; that replay matches the previously retained certificate, while an independent replay through $4000$ reproduces the unit-carry prefix. The second is an independent continued-fraction size bound.

Neither implication yields the other, and neither proves irrationality. The paper and Lean proof give $lim inf \log L_{N} / (N^{3 / 2} \log N) \geq 2 \sqrt{2} / 3$ . This is a common-denominator theorem: it shows why clearing every summand separately cannot make the positive tail small, but says nothing by itself about the denominator after cancellation. Lean separately checks that irrationality of $S$ is equivalent to cofinally many non-unit factorial carries, and checks a finite quotient-band channel obstruction. The required cofinal carries are not produced.

A local exact calculation at the prime $12487$ exhibits two critical roots for gap $12$ , so the earlier small-prime pattern of at most one critical root is not a uniform theorem; those roots have factorial values $442$ and $6300$ , not $1$ . Lean checks the $3 / 2$ theorem as common_denominator_growth_liminf in PaperCompleteLiminf.lean. The separate public Lean release wcook04/plectis-erdos-lean states the $3 / 2$ bound at commit 52f29ad1 as common_denominator_growth in its entry PalomarCorpus/E68 and proves it; that repository’s Linux replay of Palomar’s Comparator stage accepted the entry with both kernels (run 34782407633).

Further conditional zero-branch and private-factor carry producers are in the formal evidence; neither supplies the cofinal property for the actual factorial-gap orbit. Read the short paper or long record. The separately prepared E68_05 Comparator selection contains six structural carry, channel and criterion declarations. It does not select the denominator exclusions or the $3 / 2$ growth theorem above. Its caller-side preflight passed at that exact source commit; this is not a Palomar registration.

The channel results have a direct finite use. For a finitely supported integer vector $λ$ on indices $n \geq 2$ , set $M (λ) = \sum n! λ_{n}$ and let $V_{d} (λ)$ be its factorial channel at $d$ , as defined in Section 2 of the short paper. Given a depth $D \geq 2$ , the paper classifies the moments possible when $V_{2} (λ) = \dots = V_{D} (λ) = 0$ . Its tail gcd needs only coefficients through $H = D (2 p - 1) < 2 D^{2}$ for a prime $D / 2 < p \leq D$ ; this makes the minimum positive moment a finite calculation. At $D = 4$ , the minimum is 1380, attained by $λ = (- 15318, 8176, - 710, 1518, - 253, - 88, 11)$ on indices $2, \dots, 8$ .

Direct substitution gives $M (λ) = 1380$ and $V_{2} (λ) = V_{3} (λ) = V_{4} (λ) = 0$ ; the coordinate and finite-gcd theorems prove minimality. This certificate answers which moments survive a chosen finite cancellation. It does not establish nonintegrality of the remaining tail or irrationality of $S$ . Run python3 scripts/check_erdos68_channel_moment.py for the exact integer replay of the recurrence, finite gcd, moment and three vanishing channels. The paper’s finite tail-gcd theorem extends the computed gcd to all later indices.

Read the public result guide

Short paper, 9 pages

Integer Linear Forms for a Factorial Reciprocal Series

PDFOpen the PDF, 9 pages Open as its own page Current source

In this paper

Introduction

Erdős asked whether replacing $n!$ by $n! - 1$ preserves the irrationality of the reciprocal sum [1]. The question appears as Problem 68 in Bloom’s catalogue [2].

Problem 1.1 (Erdős Problem #68). Is

S = \sum_{n \geq 2} \frac{1}{n! - 1}

irrational?

The elementary proof that $e$ is irrational clears the partial sum by a factorial and bounds the remaining positive tail. Here the first step fails: for $H_{m} = \sum_{n = 2}^{m} (n! - 1)^{- 1}$ , already $3! H_{3} = 36 / 5$ . We instead construct forms $M S + k$ , with $M, k \in Z$ , by cancelling initial weighted sums. If $S = a / q$ and $q ∣ M$ , then $M S + k$ is integral; proving it nonintegral excludes that denominator.

At depth four, the weight congruences force $115 ∣ M$ . Restricting the coefficient support to $n \geq 2$ strengthens this to $1380 ∣ M$ , and every multiple of $1380$ occurs. We determine the exact factor at every depth $D \geq 2$ and construct a vector attaining the least positive multiplier.

First allow a coefficient at index one. Theorem 2.1 constructs an integral basis by correcting adjacent factorial differences at proper divisors to isolate each weighted sum. At fixed $M$ , cancellation determines the lower basis coefficients; removing index one leaves a single equation in the higher coefficients. Theorem 3.1 reduces its infinite gcd to a calculation below $2 D^{2}$ . Bézout coefficients then construct an attaining vector. No assumption on the rationality of $S$ enters this classification.

Hančl and Tijdeman’s tail-integrality lemma treats factorial series with integer coefficients [4]. Their factorial-scaled partial sums are integers. Here the scaled partial sum need not be integral. Instead, the weight congruences give $R - M S \in Z$ (1); the assumption $S = a / q$ and $q ∣ M$ then makes $R$ integral. Koepf and Schmersau’s factorial-digit criterion [3] is used in the companion’s digit argument to give an equivalent eventual-pattern condition for $S - e + 2$ . Failure of that pattern at arbitrarily large indices also remains unproved.

Section 4 tests an attaining form; Section 5 gives the general nonintegrality test.

An integral basis

We need integer weights congruent to $n!$ modulo $d! - 1$ , with $n W_{d, n - 1} = W_{d, n}$ when $n \geq 2$ and $d ∤ n$ . Removing powers of $d!$ preserves the residue; the floor exponent gives the required jumps. Put

W_{d, n} = \frac{n!}{(d!)^{⌊ n / d ⌋}} (d \geq 2, n \geq 1) .

Writing $n = k d + r$ , $0 \leq r < d$ , shows that $W_{d, n}$ is $r!$ times the multinomial coefficient $n! / ((d!)^{k} r!)$ . Thus it is an integer, and $n! = (d!)^{k} W_{d, n}$ gives $W_{d, n} \equiv n! (\mod d! - 1)$ . For example, $W_{3, 4} = 4$ and $(4! - W_{3, 4}) / (3! - 1) = 4$ .

For a finitely supported integer vector $λ = (λ_{n})_{n \geq 1}$ , define the integer linear forms

M (λ) = \sum_{n} λ_{n} n!, V_{d} (λ) = \sum_{n} λ_{n} W_{d, n},

and let

R (λ) = \sum_{d \geq 2} \frac{V_{d} (λ)}{d! - 1} .

Here $n$ indexes coefficients and $d$ indexes remainder summands. If the support lies in $n \leq N$ , $N \geq 2$ , then $V_{d} = M$ for $d > N$ . Thus the remainder converges absolutely, and subtracting $M S$ leaves only finitely many terms. The weight congruence makes each an integer:

\begin{matrix} (1) & R (λ) - M (λ) S = \sum_{d = 2}^{N} \frac{V_{d} (λ) - M (λ)}{d! - 1} \in Z . \end{matrix}

We solve $V_{2} = \dots = V_{D} = 0$ , allowing either sign of $M$ . Write $e_{n}$ for the unit vector at index $n$ . Index one is auxiliary: it makes the basis triangular but introduces no term $1 / (1! - 1)$ , since the remainder still starts at $d = 2$ . We impose $λ_{1} = 0$ in Section 3.

The identity $n (n - 1)! - n! = 0$ suggests starting with $T_{n} = n e_{n - 1} - e_{n}$ . At $n = 2$ , the vector $U_{2} = 2 e_{1} - e_{2}$ has $V_{2} = 1$ and every other weighted sum zero. At $n = 4$ , the difference $T_{4} = 4 e_{3} - e_{4}$ has two nonzero weighted sums. One correction suffices:

Vector	$M$	$V_{2}$	$V_{3}$	$V_{4}$
$T_{4}$	$0$	$6$	$0$	$23$
$6 U_{2}$	$0$	$6$	$0$	$0$
$T_{4} - 6 U_{2}$	$0$	$0$	$0$	$23$

For $d > 4$ these weighted sums equal $M = 0$ . Thus $U_{4} = T_{4} - 6 U_{2}$ isolates $V_{4} = 4! - 1$ . In general, the unwanted sums occur at proper divisors of $n$ , whose correcting vectors are already available in an inductive construction.

Theorem 2.1 (an integer basis with prescribed weighted sums). Set

T_{n} = n e_{n - 1} - e_{n}, U_{n} = T_{n} - \sum_{\begin{matrix} d ∣ n \\ 2 \leq d < n \end{matrix}} W_{d, n} U_{d} (n \geq 2) .

Then

M (U_{n}) = 0, V_{d} (U_{n}) = (d! - 1) 1_{d = n} .

The vectors $e_{1}, U_{2}, U_{3}, \dots$ form an integral basis. Every finite vector has the unique finite expansion

\begin{matrix} (2) & λ = M (λ) e_{1} + \sum_{d \geq 2} \frac{V_{d} (λ) - M (λ)}{d! - 1} U_{d} . \end{matrix}

Proof. We have $M (T_{n}) = 0$ . If $d ∤ n$ , the floor exponents at $n - 1$ and $n$ agree, so $n W_{d, n - 1} = W_{d, n}$ . If $d ∣ n$ , the exponent increases by one, so $n W_{d, n - 1} = d! W_{d, n}$ . Hence

V_{d} (T_{n}) = (d! - 1) W_{d, n} 1_{d ∣ n} .

Suppose the asserted identities hold below $n$ . For each proper divisor $d$ , subtracting $W_{d, n} U_{d}$ cancels the sum at $d$ and changes none of the others. The sum at $n$ remains $n! - 1$ , since $W_{n, n} = 1$ . This proves the identities by induction.

For completeness, restrict to indices $1, \dots, N$ . The columns $e_{1}, T_{2}, \dots, T_{N}$ form a triangular integer matrix with diagonal $1, - 1, \dots, - 1$ . Replacing each $T_{n}$ by $U_{n}$ subtracts an integer combination of earlier columns, so the second change of basis is triangular with diagonal one. Both matrices have integer inverses: back-substitution divides only by $1$ or $- 1$ . Hence $e_{1}, U_{2}, \dots, U_{N}$ is a basis over $Z$ .

In the resulting expansion, applying $M$ gives the coefficient of $e_{1}$ . If the coefficient of $U_{d}$ is $c_{d}$ , applying $V_{d}$ gives $V_{d} = M + (d! - 1) c_{d}$ , which proves (2). For $d > N$ that coefficient is zero because $V_{d} = M$ . ◻

The $U_{d}$ -coordinates in (2) are exactly the integer summands in (1). Their sum is therefore $k$ in $R = M S + k$ .

For a prime $p \geq 3$ the divisor sum is empty, and $U_{p} = p e_{p - 1} - e_{p}$ . At a composite index the correction terms remove the extra weighted sums. For example,

\begin{matrix} (3) & U_{9} = 9 e_{8} - e_{9} - 5040 e_{2} + 1680 e_{3} . \end{matrix}

Adding $U_{n}$ changes only $V_{n}$ among the weighted sums, preserves $M$ , and adds one to $R$ . Integer multiples therefore preserve the fractional part.

Possible values of $M$

Fix $D \geq 2$ and solve $V_{2} = \dots = V_{D} = 0$ , allowing index one temporarily. The coordinates in (2) give

\begin{matrix} (4) & V_{d} (λ) \equiv M (λ) (\mod d! - 1) . \end{matrix}

It follows that $M$ must be divisible by

L_{D} = {lcm}_{2 \leq d \leq D} (d! - 1) .

This necessary condition is sufficient while index one is allowed: $L_{D} e_{1}$ has every weighted sum equal to $L_{D}$ , and subtracting $L_{D} / (d! - 1)$ copies of $U_{d}$ sets the $d$ th sum to zero without changing the others. Thus put

K_{D} = L_{D} e_{1} - \sum_{d = 2}^{D} \frac{L_{D}}{d! - 1} U_{d} .

Uniqueness of the coordinates now gives the complete solution

\begin{matrix} (5) & V_{2} = \dots = V_{D} = 0 ⟺ λ = t K_{D} + \sum_{n > D} z_{n} U_{n}, M = t L_{D}, \end{matrix}

with $t \in Z$ and finitely many nonzero integers $z_{n}$ . The coefficient of $e_{1}$ in (2) is $M$ ; the original coordinate $λ_{1}$ also receives contributions from the $U_{n}$ . Write $a_{D} = (K_{D})_{1}$ and $u_{n} = (U_{n})_{1}$ . The support restriction is exactly

\begin{matrix} (6) & t a_{D} + \sum_{n > D} z_{n} u_{n} = 0. \end{matrix}

The higher corrections leave cancellation untouched and change the first coordinate by exactly $g_{D} Z$ , where $g_{D} = gcd {u_{n} : n > D}$ . They can therefore remove $t a_{D}$ precisely when $g_{D} ∣ t a_{D}$ . For example, at depth four we shall find $a_{4} = - 55$ and $g_{4} = 60$ . Removing index one then requires $60 ∣ 55 t$ , or $12 ∣ t$ ; hence $M = 115 t$ must be a multiple of $1380$ .

In general, the possible values of $M$ form the ideal

\begin{matrix} (7) & μ_{D} Z, μ_{D} = L_{D} \frac{g_{D}}{gcd (g_{D}, a_{D})} . \end{matrix}

Indeed, division by $gcd (g_{D}, a_{D})$ leaves two coprime integers, so $g_{D} ∣ t a_{D}$ holds exactly when $g_{D} / gcd (g_{D}, a_{D}) ∣ t$ . Bézout’s identity supplies the required finite combination; the next theorem bounds the indices needed. Every vector attaining $μ_{D}$ has coefficient gcd one, since division by a common factor would give a smaller positive multiplier.

A finite gcd calculation

The recursion for the first coordinate is

u_{2} = 2, u_{n} = - \sum_{\begin{matrix} d ∣ n \\ 2 \leq d < n \end{matrix}} W_{d, n} u_{d} (n > 2) .

Induction gives $u_{n} = 0$ at odd indices and $u_{2 p} = - (2 p)! / 2^{p - 1} \neq 0$ at twice a prime, including $p = 2$ . Choose a prime $ℓ$ with $D / 2 < ℓ \leq D$ , using Bertrand’s postulate for $D \geq 3$ and $ℓ = 2$ for $D = 2$ . A finite gcd containing $u_{2 ℓ}$ is positive and divides $(2 ℓ)!$ .

The remaining issue is whether later coefficients reduce this gcd. In each recurrence term $W_{d, n} u_{d}$ , induction controls $u_{d}$ for $d > D$ . For $d \leq D$ , unordered block counting gives $(n / d)! ∣ W_{d, n}$ . The cutoff ensures $n / d \geq 2 ℓ$ , so the weight supplies the factor $(2 ℓ)!$ instead.

Theorem 3.1 (a finite formula for the gcd). Choose a prime $ℓ$ with $D / 2 < ℓ \leq D$ and put $H = D (2 ℓ - 1)$ . Then

g_{D} = gcd (u_{D + 1}, \dots, u_{H}), H < 2 D^{2} .

Proof. Let $g = gcd (u_{D + 1}, \dots, u_{H})$ . The index $2 ℓ$ belongs to this interval, and $u_{2 ℓ} = - (2 ℓ)! / 2^{ℓ - 1} \neq 0$ . Consequently $g > 0$ and $g ∣ (2 ℓ)!$ .

We prove $g ∣ u_{n}$ for every $n > D$ by strong induction. This is true up to $H$ by definition. For $n > H$ , consider a proper divisor $d \geq 2$ in the recurrence for $u_{n}$ . If $d > D$ , the induction hypothesis gives $g ∣ u_{d}$ . If $d \leq D$ , put $k = n / d$ . The choice $H = D (2 ℓ - 1)$ ensures $k \geq 2 ℓ$ . Moreover,

\frac{W_{d, n}}{k!} = \frac{n!}{(d!)^{k} k!} \in Z :

this quotient counts partitions of $n$ labelled objects into $k$ unordered blocks of size $d$ . Hence $(2 ℓ)! ∣ k! ∣ W_{d, n}$ , so $g ∣ W_{d, n}$ in the small-divisor case as well. Every product $W_{d, n} u_{d}$ in the recurrence is therefore divisible by $g$ .

Thus $g$ divides the whole tail. Conversely, every common divisor of the tail divides its finite subfamily $u_{D + 1}, \dots, u_{H}$ . The two gcds are equal, and $H \leq D (2 D - 1) < 2 D^{2}$ . ◻

The coefficient at $2 ℓ \leq 2 D$ supplies positivity; the larger cutoff controls the small-divisor weights. The argument does not justify truncation at $2 D$ .

To attain the least positive multiplier, compute integers $b_{n}$ with $\sum_{n = D + 1}^{H} b_{n} u_{n} = g_{D}$ by the extended Euclidean algorithm, and put $h = gcd (g_{D}, a_{D})$ . Taking

t = g_{D} / h, z_{n} = - (a_{D} / h) b_{n} (D < n \leq H)

makes $t a_{D} + \sum z_{n} u_{n} = 0$ . Substitution in (5) therefore gives $M = μ_{D}$ with support in $2, \dots, H$ .

The associated remainder

Fix $M \in μ_{D} Z$ and put $t = M / L_{D}$ . For choices of $z_{n}$ satisfying (6), the identities $R (e_{1}) = S$ and $R (U_{n}) = 1$ give

\begin{matrix} (8) & R (t K_{D} + \sum_{n > D} z_{n} U_{n}) = t L_{D} (S - H_{D}) + \sum_{n > D} z_{n}, H_{D} = \sum_{d = 2}^{D} \frac{1}{d! - 1} . \end{matrix}

Since $M H_{D} \in Z$ , the offset from $M S$ is $k = - M H_{D} + \sum_{n > D} z_{n}$ ; $\sum z_{n}$ alone is the offset from $M (S - H_{D})$ . All choices at fixed $M$ therefore have the same fractional part.

The least multiplier at depth four

At depth four the recursion gives

L_{4} = 115, K_{4} = - 55 e_{1} + 16 e_{2} + 3 e_{3} + 5 e_{4}, a_{4} = - 55.

Take $ℓ = 3$ in Theorem 3.1, so that $H = 20$ . Since $u_{6} = - 180$ , $u_{8} = - 4200$ and $23 u_{6} - u_{8} = 60$ , we have $g_{4} ∣ 60$ . For the converse,

\begin{matrix} (9) & lcm (1, \dots, n) ∣ u_{n} \end{matrix}

gives $60 ∣ u_{n}$ for every $n > 4$ , hence $60 ∣ g_{4}$ . To prove (9), put $Λ_{n} = lcm (1, \dots, n)$ . For a prime $r$ , write $v_{r}$ for its valuation. If $d ∣ n$ , Legendre’s formula gives

v_{r} (W_{d, n}) = \sum_{j \geq 1} (⌊ \frac{n}{r^{j}} ⌋ - \frac{n}{d} ⌊ \frac{d}{r^{j}} ⌋) \geq v_{r} (Λ_{n}) - v_{r} (Λ_{d}) .

Each summand is nonnegative, and each power $d < r^{j} \leq n$ contributes at least one. Hence $Λ_{n} ∣ W_{d, n} Λ_{d}$ , and induction in the recurrence, starting from $u_{2} = 2$ , proves the assertion. Thus $g_{4} = 60$ , and (7) gives

μ_{4} = 115 \frac{60}{gcd (60, 55)} = 1380.

To attain $M = 1380$ , take $t = 12$ in (6). The choice $z_{6} = - 27$ , $z_{8} = 1$ works because

12 (- 55) - 27 (- 180) - 4200 = 0.

The vector $12 K_{4} - 27 U_{6} + U_{8}$ therefore has no index-one coefficient and cancels $V_{2}, V_{3}, V_{4}$ . To remove its coefficients at indices four and seven, add $- 26 U_{5} + 8 U_{7}$ . These corrections still cancel through four and do not restore index one, since $u_{5} = u_{7} = 0$ . Thus

λ = 12 K_{4} - 26 U_{5} - 27 U_{6} + 8 U_{7} + U_{8},

which expands to

\begin{matrix} (10) & λ = 1482 e_{2} - 784 e_{3} - 136 e_{5} + 83 e_{6} - e_{8}, (M, V_{2}, V_{3}, V_{4}) = (1380, 0, 0, 0) . \end{matrix}

Table 1 verifies all four sums directly.

The depth-four checks: multiply each of the last four columns by $λ_{n}$ and sum to obtain the last row.
$n$	$λ_{n}$	$n!$	$W_{2, n}$	$W_{3, n}$	$W_{4, n}$
2	1482	2	1	2	2
3	-784	6	3	1	6
5	-136	120	30	20	5
6	83	720	90	20	30
8	-1	40320	2520	1120	70
Weighted totals		$1380$	$0$	$0$	$0$

The basis coordinates give the offset $- 26 - 27 + 8 + 1 = - 44$ in (8). Since $H_{4} = 143 / 115$ , the original linear form is

R (λ) = 1380 (S - H_{4}) - 44 = 1380 S - 1760.

For the remainder estimate, the inequality $(n + 1)! - 1 > (n + 1) (n! - 1)$ gives the geometric bound

\begin{matrix} (11) & 0 < S - H_{N} < \frac{N + 2}{(N + 1) ((N + 1)! - 1)} < \frac{2}{(N + 1)! - 1} (N \geq 2) . \end{matrix}

The majorant starts with $1 / ((N + 1)! - 1)$ and has ratio $1 / (N + 2)$ .

Exact rational arithmetic gives

- 31 + \frac{4}{5} < 1380 \sum_{d = 5}^{8} \frac{1}{d! - 1} - 44 < - 31 + \frac{5}{6}, \frac{2 \cdot 1380}{9! - 1} < \frac{1}{100} .

The omitted contribution to $R$ is positive and less than $1 / 100$ , so $- 31 < R (λ) < - 30$ . If $S = a / q$ with $q ∣ 1380$ , (1) would make this remainder an integer. Every divisor of $1380$ is therefore excluded.

The depth-six calculation gives $μ_{6} = 24 L_{6}$ : the extra factor need not equal $12$ . The companion also gives a dual congruence, support bounds and coefficient-norm refinements. Least multiplier, least support size and least coefficient norm are distinct problems; (7) settles only the first.

Nonintegrality of the remainder

Fix a vector with $V_{2} = \dots = V_{D} = 0$ and $M > 0$ , and choose any cutoff $N \geq D$ at or beyond its support. Separate the signed finite sum from the positive tail:

A_{N} = \sum_{d = D + 1}^{N} \frac{V_{d} (λ)}{d! - 1}, R (λ) = A_{N} + M (S - H_{N}) .

The remainder exceeds $A_{N}$ . By (11), it lies below the least integer strictly above $A_{N}$ whenever

\begin{matrix} (12) & \frac{2 M}{(N + 1)! - 1} < ⌊ A_{N} ⌋ + 1 - A_{N} . \end{matrix}

Then $⌊ A_{N} ⌋ < R (λ) < ⌊ A_{N} ⌋ + 1$ , excluding every denominator dividing $M$ . The strict successor matters: at an integral $A_{N}$ the gap is one, whereas just below an integer it can be arbitrarily small. Failure of the comparison is inconclusive.

At depth two, fix $λ = - 6 e_{2} + e_{4}$ , with $M = 12$ , and vary only the cutoff. At $N = 4$ , its finite part $A_{4} = - 239 / 115$ lies just below $- 2$ , and its gap $9 / 115$ is smaller than the bound $24 / 119$ . At $N = 5$ , the finite part $A_{5} = - 27061 / 13685$ has crossed $- 2$ : the next integer is now $- 1$ , and the gap $13376 / 13685$ exceeds $24 / 719$ . For any fixed vector with $M > 0$ , $A_{N}$ increases to $R$ . If $R$ is nonintegral, the gap tends to a positive number and the test eventually succeeds. If $R$ is integral, the eventual gap equals the omitted tail, so the strict upper-bound test fails. Changing the cutoff detects nonintegrality; it neither creates it nor changes $M$ . Coefficient changes at fixed $M$ preserve nonintegrality by (8).

To exclude every denominator, $M$ must vary. The companion’s progression construction adds size control: polynomial root conditions give primitive vectors (coefficient gcd one) with $0 < M < N!$ , where $N$ is their largest supported index. Every fixed $q$ divides their multipliers for all sufficiently large $N$ . The tail at that endpoint is below $2 / N$ , but the next-integer gap may shrink too. For each $q > 0$ , one still needs a vector with $q ∣ M$ and a cutoff satisfying (12); the cutoff may exceed its support endpoint. No minimal-support assertion is made.

The companion treats the equivalent carry condition and the complementary-denominator tail inequality. It also records two larger finite computations: a non-unit carry at $m = 300000$ excludes every $q ∣ 299999!$ , and a continued-fraction enclosure excludes every $q < 2^{39990}$ . Both computations were performed outside Lean; their algorithms, exact outputs and scope are given there. The factorial-divisibility exclusion does not exclude all denominators with only small prime factors, whose exponents may be larger. Neither finite restriction establishes the required condition at arbitrarily large indices.

Verification

The integral-basis theorem and finite gcd formula have recorded exact Lean bindings. The companion source concordance identifies their declarations and the theorem on the possible values of $M$ . Its large finite computations are separate from these kernel proofs.

Acknowledgements

An AI research pass supplied by Will Cook derived the depth-four dual congruence and shorter vectors from the weighted linear forms and the classification of their possible coefficients $M$ developed earlier here. OpenAI Codex checked and integrated them; a separate AI pass reviewed the proof.

References

Paul Erdős. On the irrationality of certain series: problems and results. In Alan Baker (ed.), New Advances in Transcendence Theory, Cambridge University Press (1988), pp. 102–109.
Thomas F. Bloom. Erdős Problem #68. Online resource (2026). Historical access: 28 July 2026; present-page status not reverified.
Wolfram Koepf and Dieter Schmersau. Irrationality of certain infinite series II. Analysis 31 (2011), 117–124.
Jaroslav Hančl and Robert Tijdeman. On the irrationality of factorial series. Acta Arithmetica 118 (4) (2005), 383–401.

Long paper, 51 pages

Factorial Linear Forms and Denominators: Detailed Proofs and Rationality Criteria

PDFOpen the PDF, 51 pages Open as its own page Current source

PDF and source links follow the latest files on GitHub. The web reader shows the edition published here.

Lean source files

60 source files, each a programme or result file. See them in the Lean map.

The programme directory, linked result sources and their local imports. Shared files can appear in more than one programme.

GitHub lean/ErdosProblems/Erdos68/AdjacentUnitCarryWindow.lean
GitHub lean/ErdosProblems/Erdos68/CanonicalFactorialDigits.lean
GitHub lean/ErdosProblems/Erdos68/CanonicalFactorialTermination.lean
GitHub lean/ErdosProblems/Erdos68/CarryCongruenceNormalForm.lean
GitHub lean/ErdosProblems/Erdos68/ChannelBreakpointRigidity.lean
GitHub lean/ErdosProblems/Erdos68/ChannelIntegralCongruence.lean
GitHub lean/ErdosProblems/Erdos68/CompanionConstantBridge.lean
GitHub lean/ErdosProblems/Erdos68/CompanionConstantCarryLaw.lean
GitHub lean/ErdosProblems/Erdos68/CompanionOrbitRationality.lean
GitHub lean/ErdosProblems/Erdos68/ConstantOnlyMissCertificates.lean
GitHub lean/ErdosProblems/Erdos68/DepthFourShortSupport.lean
GitHub lean/ErdosProblems/Erdos68/DivisorChannelBasis.lean
GitHub lean/ErdosProblems/Erdos68/DivisorFactorialCentre.lean
GitHub lean/ErdosProblems/Erdos68/EndpointWeightedPrivateSupport.lean
GitHub lean/ErdosProblems/Erdos68/FactorialAnalyticBoundary.lean
GitHub lean/ErdosProblems/Erdos68/FactorialCarry.lean
GitHub lean/ErdosProblems/Erdos68/FactorialChannelCertificate.lean
GitHub lean/ErdosProblems/Erdos68/FactorialDigitRigidity.lean
GitHub lean/ErdosProblems/Erdos68/FactorialGapPlateauCore.lean
GitHub lean/ErdosProblems/Erdos68/FactorialShiftFamilyOrbit.lean
GitHub lean/ErdosProblems/Erdos68/FactorialZeroPlateau.lean
GitHub lean/ErdosProblems/Erdos68/FactorialZeroPlateauCertificates.lean
GitHub lean/ErdosProblems/Erdos68/FactorialZeroPlateauSupplement.lean
GitHub lean/ErdosProblems/Erdos68/FiniteDefectAutomaton.lean
GitHub lean/ErdosProblems/Erdos68/FiniteLeadBlocks/Size000.lean
GitHub lean/ErdosProblems/Erdos68/FiniteLeadBlocks/Size001.lean
GitHub lean/ErdosProblems/Erdos68/GapScalarNormalForm.lean
GitHub lean/ErdosProblems/Erdos68/MultiplicativeSuccessorRigidity.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteAsymptotics.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteDivisorCoordinates.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteDyadicEnclosure.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteExisting.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteFiniteLeadArithmetic.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteFiniteSizeCertificate.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteFiniteSizeData.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteIntegerSpan.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteKernelFloorAlgorithm.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteKernelFloorSoundness.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteKernelSizeSum.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteLiminf.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteLowKernel.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteMomentHorizon.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteMomentIdeal.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompletePrimePole.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteRadiusLimit.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteResidualIdentity.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteSupplementary.lean
GitHub lean/ErdosProblems/Erdos68/PaperCompleteSupportedBands.lean
GitHub lean/ErdosProblems/Erdos68/PaperCorrespondenceAudit.lean
GitHub lean/ErdosProblems/Erdos68/PaperCorrespondenceAuditAdditive.lean
GitHub lean/ErdosProblems/Erdos68/PolynomialPerturbationLcm.lean
GitHub lean/ErdosProblems/Erdos68/PrimePoleCriterion.lean
GitHub lean/ErdosProblems/Erdos68/PrimePoleDenominator.lean
GitHub lean/ErdosProblems/Erdos68/PrimeThresholdParity.lean
GitHub lean/ErdosProblems/Erdos68/PrimeUnitTranslator.lean
GitHub lean/ErdosProblems/Erdos68/PrimeZeroBranch.lean
GitHub lean/ErdosProblems/Erdos68/SecondLayerDigit.lean
GitHub lean/ErdosProblems/Erdos68/ShrinkingTargetNormalForm.lean
GitHub lean/ErdosProblems/Erdos68/StrictSuccessorArithmetic.lean
GitHub lean/ErdosProblems/Erdos68/TailIdealCertificate.lean

Statements with Lean proofs

Lean is software that verifies a formal proof against its theorem statement and assumptions. These proofs establish only the statements listed here.

The exact integral normal form: the series is irrational if and only if the strict factorial successor $Z_{m}$ misses divisibility by m cofinally.
The equivalent carry form: rationality is equivalent to eventual unit carry, so cofinally many non-unit carries imply irrationality.
Canonical factorial digits, exact remainder recurrences, zero-tail propagation, and the divisor-factorial centre recurrence.
Integral channel congruences, the lcm tax, the prime unit translator, and factorial-grid Cramer residual identities.
Weighted projection and factor-split rigidity consumers with their exact modular and Archimedean hypotheses.
The zero-plateau and first-exit carry dichotomy, prime-power prefix obstructions, and exact doubled-prime branch characterisations.
A Lean-checked implication from one exact non-unit carry to a rational-denominator lower bound; a fresh exact GMP certificate at $m = 300000$ supplies the finite input used by the papers; the event-trace and unit carries match the previously retained receipt.

What these proofs do not establish

Irrationality of the factorial-denominator series.
A theorem producing cofinally many divisibility misses or non-unit carries.
Cofinal strict nonintegrality of the factorial-grid Cramer residual.
The weighted collision-product and complementary-residue estimates needed by the factor-split projection consumer.
The GMP computation is an exact finite external certificate, not a Lean evaluation and not an unbounded argument.

The formal record: 2 main results, 5 open obligations, 13 selected result modules, finite search evidence, Comparator review

Main results

Statements and their limits are copied from the public research record. Recorded status: registered_declarations

locally proved result; novelty unassessed family: factorial_carry_characterisation

Irrationality is equivalent to cofinally many strict-successor divisibility failures.

The equivalence does not prove that the cofinal failures occur.

ErdosProblems.Erdos68.irrational_factorialGapSeries_iff_cofinal_strictFacTopRat_misses

locally proved result; novelty unassessed family: factorial_carry_characterisation

Irrationality is equivalent to cofinally many non-unit carries.

The equivalence does not supply a cofinal carry producer.

ErdosProblems.Erdos68.irrational_factorialGapSeries_iff_cofinal_nonunit_carries

Assumptions still needing proofs

Prove any one of these and the corresponding reduction above becomes unconditional.

weighted_collision_and_complementary_residue On an unbounded family of tailored prime blocks, prove both the weighted collision-core product bound and the independent complementary-residue inequality consumed by the exact unit-factor scale split.
cofinal_prime_power_amplification At infinitely many genuinely nonterminal indices, prove quantitative repeated-support valuation amplification strong enough to meet the checked endpoint inequality.
cofinal_lower_endpoint_escape For infinitely many primes, force the reduced predecessor gap outside the exact lower unit-carry cylinder.
cofinal_doubled_prime_branch_failure For infinitely many odd primes, rule out both exact p²-divisibility branches at index 2p by coupling the carry value to the predecessor residue.
cramer_residual_nonintegrality Construct an unbounded factorial-grid family whose exact Cramer residual is nonintegral, using a determinant, valuation, cancellation, or gcd-of-minors certificate that controls the finite sign-changing block.

Finite search evidence

A retained exact GMP receipt through $m = 300000$ records a non-unit carry at that index, so every positive rational denominator satisfies q ∤ $299999! .$ A byte-identical regeneration of that receipt with the current driver is outstanding in this revision; a separate exact replay through 4000 reproduces the unit-carry prefix. The Lean consumer turns one non-unit carry at m into $q \geq m$ ; it does not prove a cofinal statement. An independent continued-fraction enclosure gives $q \geq 2^{39990}$ . At the prime 12487 and gap 12, exact polynomial arithmetic exhibits two critical roots 4626 and 7848, so the small-prime pattern of at most one critical root is not uniform; those roots have factorial values 442 and 6300, not 1.

Selected Lean proof files

The public result record selects 13 modules. Browse all 60 source files in this programme’s source map, including shared result sources and local imported dependencies.

Module	Lines	Declarations	Theorems
`ErdosProblems.Erdos68.FactorialGapPlateauCore`	1008	36	31
`ErdosProblems.Erdos68.CanonicalFactorialDigits`	278	18	15
`ErdosProblems.Erdos68.ChannelBreakpointRigidity`	144	10	8
`ErdosProblems.Erdos68.ChannelIntegralCongruence`	1198	58	49
`ErdosProblems.Erdos68.DivisorFactorialCentre`	303	18	13
`ErdosProblems.Erdos68.EndpointWeightedPrivateSupport`	6675	223	183
`ErdosProblems.Erdos68.FactorialCarry`	101	8	5
`ErdosProblems.Erdos68.FactorialChannelCertificate`	172	17	11
`ErdosProblems.Erdos68.FactorialZeroPlateau`	37	0	0
`ErdosProblems.Erdos68.FiniteDefectAutomaton`	120	10	6
`ErdosProblems.Erdos68.PrimeUnitTranslator`	1730	91	70
`ErdosProblems.Erdos68.PrimeZeroBranch`	7293	187	155
`ErdosProblems.Erdos68.StrictSuccessorArithmetic`	204	4	4

Comparator review

Comparator runs selected Lean proofs against separately supplied theorem statements using recorded software versions. A successful run establishes that those proofs satisfy those statements; it does not prove the unanswered questions above.

Replayed by the Comparator

Statement and type parity replayed against the pinned toolchain.

Exact equivalence between irrationality, cofinally many non-unit carries, and cofinal strict-successor divisibility failures.

An exact reformulation does not supply the required cofinal failures.

factorial_carry_characterisation: targeted

Represented indirectly

Covered through a neighbouring selected interface, not replayed one-to-one.

Finite quotient-band channel factorisation and breakpoint, channel congruences, a two-term prime-channel corrector, and endpoint-weighted projection rigidity.

These finite and structural results do not produce a cofinal obstruction.

factorial_channel_and_projection_rigidity: represented_by_isolated_headline

Outside the Comparator selection

Stated in the corpus; not part of the replayed interface set.

Cofinal zero-branch or large private-factor hypotheses imply the required irrationality conclusion.

The producer hypotheses are unproved.

factorial_conditional_producers: not_selected_deep_project_predicate_stack
Lean checks small exact misses; a hash-bound GMP scan reaches index 300000 and yields the corresponding finite denominator exclusion.

Finite computation does not change the cofinal quantifier.

factorial_finite_certificates: not_applicable_to_external_execution
An elementary terminal-block argument gives liminf log $L_{N} / (N^{3 / 2} \log N) \geq 2 \sqrt{2} / 3$ for the lcm of factorial-gap denominators. The displayed bound needs no external multiplicity theorem; an older, weaker multiplicity-based route is historical context only.

The LCM asymptotic has an ordinary paper proof and is checked in Lean as common_denominator_growth_liminf in PaperCompleteLiminf.lean. The finite-block inequality has a separate Lean source. The Comparator entry for this bound belongs to the separate public release wcook04/plectis-erdos-lean. The bound does not decide irrationality.

factorial_lcm_growth: not_selected_separate_release_comparator_entry

The result statements, their limits and the counts are copied from the public Lean repository’s published records identified by b0ebeb9add157584. These records are copied into the page when the website is built. Introductory explanations and labels are written for this site. The diagram at the top is the exception: a program draws it from numbers the papers print and tests the numerical relationships shown. Its caption and explanation are written for this site.