Is $\sum_n \phi(n)/2^n$ irrational, where $\phi$ is Euler's totient? (Erdős #249)
Statement
Let $\phi$ be the Euler totient function, so $\phi(n)$ counts the integers in $\{1,\dots,n\}$ that are coprime to $n$. Is the real number $$\sum_{n=1}^{\infty}\frac{\phi(n)}{2^n}$$ irrational? The series converges absolutely (since $\phi(n)<n$), and the question is purely whether its value is a rational number.
Acceptance. FULLY RESOLVES: a complete, rigorous proof that $\sum_n \phi(n)/2^n$ is irrational, OR a proof that it is rational together with its exact rational value — a machine-checkable Lean/Coq formalisation is preferred (a formal statement already exists in the DeepMind formal-conjectures repository), otherwise a full written proof with every step and constant explicit. A numerical computation of the digits alone can NEVER close this problem. ADVANCES (each itself checkable): a rigorous partial result — for instance an effective irrationality measure, or a proof that the value has no rational representation with denominator below an explicit bound; an irrationality proof conditional on a clearly-stated standard conjecture; or a proven new closed form/identity (e.g. sharpening $\sum_n\phi(n)x^n=\sum_d\mu(d)x^d/(1-x^d)^2$) that provably reduces the question to a stated checkable sub-problem — strictly beyond what the background records (which is: no partial result known). Deliver the Lean proof file or a complete written proof with all steps.
Background
Posed by Erdős and recorded in Erdős–Graham [ErGr80, p.61] and Erdős [Er88c, p.102]; listed as open on erdosproblems.com/249 (fetched 2026-07-13, status 'open', tagged 'number theory | irrationality'), with no prize attached. The decimal expansion of the sum is catalogued as OEIS A256936, and a machine-checkable formal statement of the conjecture already exists in DeepMind's formal-conjectures Lean library. The problem belongs to a well-known cluster of Erdős irrationality questions about arithmetic-function generating values at rational points — compare Erdős #251 (erdosproblems.com/251) on $\sum p_n/2^n$ and Erdős #252 (erdosproblems.com/252) on $\sum \sigma_k(n)/n!$ — but, unlike those, no partial or conditional irrationality result is on record for this specific sum. A concrete analytic handle comes from $\phi=\mu\ast\mathrm{Id}$: one gets the identity $\sum_{n\ge1}\phi(n)x^n=\sum_{d\ge1}\mu(d)\,x^d/(1-x^d)^2$, so at $x=1/2$ the value equals $\sum_{d\ge1}\mu(d)\,2^d/(2^d-1)^2$, a Möbius-weighted lacunary series whose arithmetic is the crux. Because irrationality is not a finite certificate, no amount of digit computation can settle it; the attacker's tool is analytic irrationality machinery — generating-function/Lambert-series identities, gcd and denominator-growth arguments on truncations, or a criterion formalised in Lean — with high-precision extension of A256936 serving only as supporting evidence.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #249 (T. F. Bloom) | website |
| REF-02 | OEIS A256936 — decimal expansion of sum_{n>=1} phi(n)/2^n | website |
| REF-03 | DeepMind formal-conjectures — Lean statement of Erdős #249 | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.