Is $\sum_{n\ge 2} 1/(n!-1)$ irrational? (Erdős #68)
Statement
Is $$\sum_{n\ge 2}\frac{1}{n!-1}$$ irrational?
Acceptance. FULLY RESOLVES: a proof that $\sum_{n\ge 2}1/(n!-1)$ is irrational (a proof of the stronger transcendence also qualifies), OR — should the sum somehow be rational — an exhibited and certified rational value. A machine-checkable Lean 4 proof extending ErdosProblems/68.lean is the gold standard; otherwise a complete written proof with every step. ADVANCES: a genuine partial result — e.g. a proof that $\sum 1/(n!+t)$ is irrational (or transcendental) for some specific integer $t$, or a nontrivial irrationality-measure / linear-independence statement for the associated factorial series, with proof. Deliver the Lean proof file or manuscript. Note: computing further decimal digits of the constant (OEIS A331373) does NOT by itself constitute progress toward irrationality.
Background
Asked by Erdős in several problem papers ([Er68d], [Er88c, p.102], [Er90], [Er97e], [Er97f]); listed as open on erdosproblems.com/68 (fetched 2026-07-13, status 'open', tagged 'number theory | irrationality'). The decimal expansion of the constant is OEIS A331373. Weisenberg observed the identity $\sum_{n\ge 2}1/(n!-1)=\sum_{k\ge 1}\sum_{n\ge 2}1/(n!)^k$, obtained by expanding $1/(n!-1)=\sum_{k\ge 1}(n!)^{-k}$. Erdős conjectured more strongly in [Er88c] that $\sum 1/(n!+t)$ should be transcendental for every integer $t$; the present problem is the case $t=-1$, where even irrationality is open. (For comparison, $\sum_{n}1/n!=e-1$ is transcendental, but the shifted denominators $n!-1$ remove the clean telescoping structure.) The statement is formalised in Lean (DeepMind Formal Conjectures, ErdosProblems/68.lean). Attacker's tool: irrationality criteria for rapidly converging series with factorial denominators (Diophantine approximation, plus the double-series reorganisation above), ideally certified via the existing Lean 4 formalisation.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #68 (T. F. Bloom) | website |
| REF-02 | OEIS A331373 — decimal expansion of the sum of 1/(n!-1) for n >= 2 | website |
| REF-03 | Lean formalisation of Erdős #68 (DeepMind Formal Conjectures) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.