Let $c > 0$ . If $x$ is sufficiently large then does there exist $n \leq x$ such that the values of $ϕ (n + k)$ are all distinct for $1 \leq k \leq (lo g x)^{c}$ , where $ϕ$ is the Euler totient function?

Worked, still open.

number theory · open · possible · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

This is **open in general** (it’s listed as an open Erdős problem, #1004). ([Erdős Problems][1])

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

AMS 11 · open (literature)

theorem erdos_1004 :
    answer(sorry) ↔ ∀ c > (0 : ℝ), ∀ᶠ x in atTop, ∃ n ≤ x,
      IsDistinctTotientRun n ⌊(Real.log (x : ℝ)) ^ c⌋₊

open