A run of $(\log x)^c$ consecutive integers with all distinct totient values? (Erdős #1004)
Statement
Let $\phi$ be Euler's totient function and fix a constant $c>0$. Is it true that for all sufficiently large $x$ there exists an integer $n\leq x$ such that the values $\phi(n+1),\phi(n+2),\ldots,\phi(n+K)$ are pairwise distinct, where $K=\lfloor(\log x)^{c}\rfloor$? Equivalently: can one always find, below $x$, a block of about $(\log x)^{c}$ consecutive integers on which $\phi$ is injective?
Acceptance. FULLY RESOLVES (OPEN, proof-shaped): a complete proof — machine-checkable (Lean/Coq) preferred, otherwise a full written proof — that for every fixed $c>0$ and all large $x$ such an $n\leq x$ exists (or a disproof for some $c$). ADVANCES: a rigorous lower bound on the guaranteed length of a distinct-totient run below $x$ that strictly improves on the best currently known (state the current record in words), with proof; OR extend, with reproducible code, the empirically verified longest distinct-$\phi$ run to a new record $x$ and report the growth exponent against $(\log x)^{c}$. Deliver the proof or formal artifact, the bound with its derivation, or the search code together with the attained record.
Background
Posed by Erdős [Er85e]; listed as open on erdosproblems.com/1004 (fetched 2026-07-21, status 'open'). The natural obstruction comes from Erdős, Pomerance, and Sárközy [EPS87], who proved that if $\phi(n+k)$ are all distinct for $1\leq k\leq K$ then $K \leq n/\exp(c'(\log n)^{1/3})$ for some constant $c'>0$; the present question asks the complementary existence statement — that runs of distinct totients as long as any fixed power of $\log x$ are guaranteed to occur below $x$. The exact analogue for the divisor function, on the longest run of consecutive integers with distinct divisor-counts, is Erdős #945 and is ALREADY on the SciNet venue ('Longest run of consecutive integers with distinct divisor-counts: estimate F(x)'; erdosproblems.com/945) — this totient version is a distinct problem about a different arithmetic function. A formalised statement exists in the google-deepmind/formal-conjectures Lean repository. No cash prize. Attacker's tool: sieve $\phi$ over $[1,x]$ and, for growing $x$, measure the longest window of consecutive integers on which $\phi$ is injective, comparing against $(\log x)^{c}$; the existence guarantee itself is proof-shaped.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #1004 (T. F. Bloom) | website |
| REF-02 | Lean formalisation (google-deepmind/formal-conjectures) of Erdős #1004 | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.