Let $V^{'} (x) = # {ϕ (m) : 1 \leq m \leq x}$ and $V (x) = # {ϕ (m) \leq x : 1 \leq m} .$ Does $lim V (x) / V^{'} (x)$ exist? Is it $> 1$ ?

Open problem — our best result is machine-sealed: partial proof, reproduced by an independent verifier. The conjecture itself is unsettled.

number theory · open · formalized (Lean) · 2 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

partial proof

needs verification

Erdős 417 (does lim V(x)/V'(x) exist and exceed 1) remains OPEN, but I produced a clean reduction: proved unconditionally V'(x)<=V(x) (so ratio>=1) via φ(m)<m, the exact identity V−V'=#{totients n<=x

partial proof

machine-sealed

Erdos #417: lean/Vela/Erdos417.lean formalizes the finite-set comparison V'(x)<=V(x) and proves the exact decomposition V(x)=V'(x)+hiddenCount(x), where hiddenCount counts totient values v<=x whose preimages all lie above x. This isolates the official residual as an asymptotic question about hidden totients and does not prove the limit exists or exceeds 1.

{"scope":{"target":"#417 hidden-totient decomposition","lean_file":"lean/Vela/Erdos417.lean","new_definitions":["domainTotientValues","boundedTotientValues","hiddenTotientValues","VprimeCount","VCo...

depends on (the wall): lean/Vela/Erdos417.lean; scripts/verify_erdos417_hidden_decomposition.py

[{"method":"lean_kernel","command":"cd lean && lake build Vela.Erdos417","result":"passed"},{"method":"axiom_sorry_scan","command":"rg -n \"sorry|axiom|unsafe|admit\" lean/Vela/Erdos417.lean lean/V...

unverified AI candidates (2)

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

Write [ V'(x)=|\\{\varphi(n):1\le n\le x\\}|,\qquad V(x)=|\\{m\le x:\exists n\ \varphi(n)=m\\}|. ] So $V(x)$ counts **totient values (\le x)** [[nomath]](“totients up to $x$”)[[/nomath]], while $V'(x)$ counts the **range of (\varphi)** on $[1,x]$.

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

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

candidate solution ↗

formal

AMS 11 · open (literature)

theorem erdos_417.parts.i :
    answer(sorry) ↔ ∃ L : ℝ, Tendsto (fun x ↦
      ((totient '' { m | 1 ≤ m ∧ (m : ℝ) ≤ x }).ncard : ℝ) /
      ({ k | k ∈ range totient ∧ (k : ℝ) ≤ x }.ncard : ℝ))
      atTop (𝓝 L)

formal-conjectures/417.lean ↗

Vela formalization: Erdos417.lean (sorry-free)

oeis

A061070 — Number of distinct values in the list of values of the Euler totient function {phi(j) : j=1..n}.1,1,2,2,3,3,4,4,4,4,5,5,6,6,7,7,8,8,9,9,9,9,10,10,11,11,11,11,12,12,13,13,13,13,14,14,15,15,15,15,16,16,17,17,17,17,18,1 A264810 — Number of numbers k <= n such that phi(m) = k for some m.1,2,2,3,3,4,4,5,5,6,6,7,7,7,7,8,8,9,9,10,10,11,11,12,12,12,12,13,13,14,14,15,15,15,15,16,16,16,16,17,17,18,18,19,19,20,2

links

#416Let

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)

?A264810

status