Let $V (x)$ count the number of $n \leq x$ such that $ϕ (m) = n$ is solvable. Does $V (2 x) / V (x) \to 2$ ? Is there an asymptotic formula for $V (x)$ ?

Worked, still open.

number theory · open · 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

Let [ V(x)=|\\{n\le x:\exists m\text{ with }\varphi(m)=n\\}|, ] i.e. $V(x)$ counts the **distinct totients** (\le x).

llm-hunter · gpt pro 5.2 · unverified

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

AMS 11 · open (literature)

theorem erdos_416.parts.i :
    Filter.Tendsto (fun x => (V (2 * x) / V (x))) Filter.atTop (𝓝 2)

V^{'} (x) = # {ϕ (m) : 1 \leq m \leq x}

V (x) = # {ϕ (m) \leq x : 1 \leq m} .

lim V (x) / V^{'} (x)

> 1

open