Erdős Problem #416

OPENdatabase updated 2025-08-31

No proof or disproof is known, and it isn't known whether a finite computation could settle it.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

Let `V(x)` count the number of `n≤x` such that `ϕ(m)=n` is solvable.

Let `V(x)` count the number of `n≤x` such that `ϕ(m)=n` is solvable. Does `V(2x)/V(x)→2` ? Yes. This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof, which gives `V(cx)/V(x)→c` for every fixed `c>0`.

Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 6 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/416.

Newer public claim (6 Oct 2026): OpenAI's internal-model release claims, for this problem, an asymptotic equivalent for the number of totient values V(x), and V(cx)/V(x) → c for every c > 0 (Erdős–Hall) — refereed here 21 Oct, see /day/416-openai-totient-count-asymptotic-refereed — family 24 at github.com/openai/math, OpenAI's own Lean proves Theorem 2.1 (V(x) ~ (x/log x)·G_m·A(θ) with A a uniform limit of finite inclusion–exclusion sums, bounded above and below, and V(cx)/V(x) → c for every c > 0), the least-preimage companion Theorem 2.2 with its zero case, and the k = 1, 2 seeds; on the way it proves Ford's order of magnitude in the paper's form, V(x) ≍ (x/log x)·G_m, rather than citing it. Replayed on our machine on 21 Oct 2026: 809 OpenAI modules + 11 of PrimeNumberTheoremAnd + 9 of LeanArchitect compiled with 0 errors (Mathlib from its cache; a fresh leanchecker pass exited 0), standard axioms, and all five theorem statements and their definitions (32 and 22) matched to the two comparator challenges under pp.all. A kernel-checked bridge of ours derives from it verbatim copies of Formal Conjectures' erdos_416.parts.i and erdos_416.variants.regularly_varying — see our /day entry. Bloom calls these claims, not endorsements.

Prizenone

Topicsnumber theory

Statement in LeanFormal Conjectures

Solution in Leanno

OEISA264810

Original pageerdosproblems.com/416

Attempts

submit one →

FULL WRITE-UP BY THIS SITE · OCT 21, 2026

Read our full write-up →

Let V(x) count the distinct values of Euler's φ up to x. Erdős asked whether V(2x)/V(x) → 2 and whether V(x) has an asymptotic formula; Erdős and Hall had asked whether V(cx)/V(x) → c. Ford (1998) knew V(x) only up to a bounded factor. OpenAI's preprint (dated 25 September, released 6 October) proves V(x) ~ (x/log x)·G_m·A(θ), an explicit scale times a bounded positive coefficient of a phase θ, and with it V(cx)/V(x) → c for every c > 0. Its Lean proof, 809 modules that also prove Ford's order of magnitude in the paper's form V(x) ≍ (x/log x)·G_m, replays on our machine with the standard axioms and statements that match its comparator files exactly. Our bridge derives from it verbatim copies of Formal Conjectures' statements. Two hostile AI referee seats, reading §§2–7 (the whole proof) between them, found no false or unjustified step; a third checked the introduction's citations and the other sources, and a fourth attacked our own additions. Part (i) was not first proved publicly by OpenAI: a Lean proof of exactly Formal Conjectures' statement, by the solver JenW1N on conjectures.io, was verified there on 14 September and published on 16 September. Ours, first: the bridge, and counts of V(x) to 10⁹ (by two independent methods up to 10⁸) that agree with every published value we found. Second, a check that the explicit scale is Ford's up to a bounded factor, and a consequence of the theorem the paper does not state, found with seat O: Ford's unknown bounded factor becomes a continuous periodic function of 2C₀(log₃x − log₄x), so the coefficient A is continuous but not constant. Third, a search for the seeds that decide the least-preimage question (for every k at once, that question is Erdős #51): none for k = 3 below 10⁹, where the largest ℓ(d)/d is 2.0434.

CLOSED

← #415 the board #417 →