#416: V(cx)/V(x) → c and an asymptotic equivalent for the number of totient values — OpenAI's proof, refereed and Lean-replayed here; part (i) was first proved publicly, in Lean, on conjectures.io

The problem (erdosproblems.com/416; [Er74b], [Er79e], [ErGr80], [Er98]). In Formal Conjectures' wording: "Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Does V(2x)/V(x)→2?" and "Is there an asymptotic formula for V(x)?" Pillai (1929) proved V(x) = o(x), and Erdős (1935) proved V(x) = x(log x)^−1+o(1). Maier and Pomerance (1988) found the leading term of the exponent, V(x) = (x/log x)·exp{(C₀ + o(1))(log₃ x)²} with C₀ = 0.8178…, and Ford (1998) sharpened this to an estimate with only a bounded factor unknown:

V(x) = (x/log x) · exp{ C₀(log₃x − log₄x)² + D₀ log₃x − (D₀ + 1/2 − 2C₀) log₄x + O(1) }

(log_k is the k-fold logarithm, D₀ = 2.1769…). That leaves both questions open: an O(1) in the exponent hides any limit of V(2x)/V(x). Ford also proved V(cx) − V(x) ≍ V(x) for each fixed c > 1. Erdős and Hall had asked earlier whether V(cx)/V(x) → c, and in [Er79e] Erdős asked a third question: how many v ≤ x have their least preimage ℓ(v) = min{n : φ(n) = v} in (kx, (k+1)x]? We wrote a working report on this problem in July (a reduction to primitive totients, a block-averaged limit, and V computed to 2²⁵); it did not settle either question.

The claim. OpenAI's family 24 (item 24 of the math release OpenAI published on 6 October) is one preprint, "An asymptotic formula for the number of totients" (dated 25 September, 39 pp). Put a_j = (j+1)log(j+1) − j log j − 1, let ρ ∈ (0,1) solve Σ_j≥1 a_jρ^j = 1, λ = log(1/ρ), γ = (Σ j a_jρ^j)⁻¹, g₀ = 1, g_j = Σ_d=1^j a_dg_j−d, and with B = log log x let m = ⌊(log B − log log B)/λ⌋, θ the fractional part of the same number (the "phase"), and G_m = B^m/(m!·g₁⋯g_m). Theorem 2.1: there are functions A_H(1; s) on [0, 1), each a finite inclusion–exclusion sum, converging uniformly to a function A(1; s) with 0 < inf A ≤ sup A < ∞, and

V(x) ~ (x/log x) · G_m · A(1; θ),        V(cx)/V(x) → c  for every fixed c > 0.

Theorem 2.2 is the least-preimage companion. For each k ≥ 1 the count N_k(x) of totients v ≤ x with kx < ℓ(v) ≤ (k+1)x satisfies N_k(x) = (x/log x)G_m(A(f_k; θ) + o(1)). If some totient d has ℓ(d) > kd (a "seed"), then N_k(x) ≍ V(x); if none does, N_k is identically 0. Seeds exist for k = 1 and 2. For k ≥ 3 the paper says plainly that it does not know which k have seeds, and that seeds for every k is equivalent to ℓ(d)/d being unbounded, a question Erdős asked elsewhere ([5, §I.9] in the paper).

The argument. Write a typical preimage as a product of primes p₀ > p₁ > … . Ford's structure theorems (his Theorems 10 and 16) say that outside a small exceptional set, every preimage of a value has log log p_i close to a prescribed profile, so the double logarithms of the large primes fill a simplex whose volume gives Ford's scale (x/log x)G_m. The paper splits each preimage into a long "prefix" of large primes, counted by volume, and a short arithmetic "tail" of at most H bounded primes and an integer, kept exactly. Different tails can give the same totient, so it counts the union of the regions they allow, by inclusion–exclusion; that union is the coefficient A_H. The hard part is showing that two different long prefixes almost never give the same totient (§§4–5): a layered sieve comparison of products of shifted primes in the style of Maier–Pomerance and Ford, needing only two or three linear forms at a time. Regular variation comes first and separately (Proposition 6.1 counts the largest prime with the same endpoint parameters at x and at x/c), and the identification with A comes after. Neither step uses continuity of A in the phase.

The Lean, and our replay. The release carries a Lean proof of Theorem 2.1 and Theorem 2.2: totient_asymptotic_formula, weighted_totient_asymptotic, weighted_totient_one_two and coefficient_nonnegative in UnconditionalMain.lean, and the zero case companion_zero_case. Their comparator challenges are ComparatorChallenges/TotientAsymptotic.lean and TotientCompanionZero.lean: OpenAI's files stating the theorems, with the proofs left as sorry, for a solution to match. The proof is 809 OpenAI modules (72,764 lines; 757 theorems and 1,888 lemmas) on Lean 4.34.1 and Mathlib d13f23b7. It also imports 11 modules of the PrimeNumberTheoremAnd project (PNT+) at c39a751, 8,632 lines covering the prime number theorem by Wiener's method, Mertens' theorems and the Selberg sieve, and 9 modules of LeanArchitect at 468e8f5, the metaprogramming package behind the blueprint attributes PNT+ uses. Our source audit of the 809 OpenAI modules found no axiom, sorry, admit, native_decide, set_option, macro, elab, syntax, unsafe, implemented_by, extern, opaque, partial def or #eval. The word decide occurs 31 times: 20 by decide proofs of small finite facts (for example that no n < 15 has φ(n) = 8, so ℓ(8) = 15) and 11 Boolean filters. In the third-party code, PNT+'s Wiener.lean has two lemmas proved by sorry, and LeanArchitect sets debug.skipKernelTC inside its blueprint-extraction routine and defines a sorry_using tactic. No module the theorems import calls LeanArchitect's kernel-skipping extraction routine or its sorry_using tactic, and the axiom check below shows that the two sorry lemmas are never used. Our replay compiled all 829 modules from source, without lake. A first launch passed one global option to every package, failed one LeanArchitect module, and was relaunched with each package's own options; the 8 modules it had already built were kept. The relaunch built the other 821 with 0 errors in 30 min 25 s of wall time (12:06–12:37 UTC on 21 October), running at most five lean processes at once. The slowest module took 62.5 s (PNT+'s Wiener.lean), and the largest peak in any one process was 7.05 GiB. #print axioms gives exactly propext, Classical.choice and Quot.sound for all five theorems, for the two-sided bound V(x) ≍ (x/log x)·G_m and for the k = 2 seed. The four theorem types and all 32 definitions they unfold through, from IsTotient, V and ℓ to the witness sets, A_H, A and the main term, print identically in the challenge and in the solution under pp.all, Lean's fully explicit printing, which lets two statements be compared exactly. So do companion_zero_case and its 22 definitions. We mutation-tested the matcher seven ways, and each gave the expected verdict: a changed numeral in a definition, a changed interval in the theorem, a challenge without sorryAx (once per challenge file), a solution with an extra axiom, a missing definition (which must exit with "cannot see", not "mismatch"), and the unmodified logs. A first version of one mutation had silently failed to apply; the harness now refuses any mutation that leaves its input unchanged. A planted sorry is reported as sorryAx, the axiom Lean records for a missing proof, and the companion theorem applied at k = 0 fails to typecheck. Mathlib's compiled files came from its cache, so we then ran leanchecker --fresh over the whole closure of our bridge below. That closure imports UnconditionalMain, so it covers all 809 OpenAI modules of the proof (two further files in the directory, Main.lean and CofactorRowDeviation.lean, are outside it), the PNT+ and LeanArchitect modules, Mathlib and the bridge, and leanchecker re-checks every declaration from scratch, which also catches anything added with the kernel check switched off. It exited with code 0 after 3,621 s (peak memory 8.6 GiB); a missing-module control exits 1.

What the Lean proves on the way. UnconditionalMain.lean assembles the theorems from a conditional core (conditional_main_theorem_of_structure) applied to nine named inputs, and every input is a theorem proved in the closure, not a hypothesis. The paper cites Ford's Theorems 1, 10 and 16 and several of his lemmas as black boxes. The Lean proves what it uses. It proves Ford's order of magnitude in the paper's form, V(x) ≍ (x/log x)·G_m (ford_scale_lower and ford_scale_upper; the paper's (3.4)). It does not state Ford's exponent form (1.1), whose link to G_m goes through Ford's Lemmas 3.4 and 3.7. And in place of Ford's Theorem 10 it proves the exceptional-set estimate the argument needs (extractedStructureInput). A file FordInputs.lean does state versions that take Ford's Theorem 10 as a hypothesis (main_from_ford_inputs (h10 : FordTheorem10Input)), but the comparator theorems do not go through them. The Lean shows that ρ is a genuine root of the renewal equation (rho_mem; separate lemmas give 3/7 < ρ < 2/3), so the definitions are not resting on a junk value. It settles the k = 2 seed by hand: every preimage of 2¹⁸·257 is even and divisible by 257², so ℓ(2¹⁸·257) = 135,268,352 (seed_least_preimage), the value our counts give. The prime number theorem comes from PNT+'s Wiener-method proof (WeakPNT), Mertens' theorems from PNT+'s IEANTN.Mertens, and the sieve bounds for two and three linear forms from PNT+'s Selberg sieve. Mathlib at this commit has none of Ford's results. The earlier conjectures.io Lean formalizes parts of Ford's structure (his normality predicate, his polytope and his Lemma 3.2); we have not checked whether it, or anything else, proves his bound.

Formal Conjectures, and the bridge (ours). Formal Conjectures (FC) states part (i), and the general dilation, as

noncomputable abbrev V (x : ℝ) : ℝ :=
  open scoped Classical in
  (Finset.Icc 1 ⌊x⌋₊ |>.filter (fun n => ∃ (m : ℕ), m.totient = n)).card

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

theorem erdos_416.variants.regularly_varying (c : ℝ) (hc : 0 < c) :
    Filter.Tendsto (fun x => V (c * x) / V x) Filter.atTop (𝓝 c)

both tagged research solved since 11 October, with OpenAI's UnconditionalMain.lean linked as the formal proof. FC's V allows the preimage m = 0, OpenAI's requires 0 < m; they count the same set because φ(0) = 0 and only n ≥ 1 are counted. Our Bridge416.lean copies FC's definition and both statements verbatim (checked by a script, whose own mutation control fails as it should), proves the two counting functions equal, and derives both FC statements from OpenAI's theorem. #print axioms gives the standard three for both FC statements and for V_eq. The controls: changing FC's set to ask for φ(m) = n + 1 breaks V_eq, and changing the limit in parts.i from 2 to 3 breaks that proof. Neither compiles. FC's part (ii), erdos_416.parts.ii ("is there an asymptotic formula"), stays research open there; see below. (FC also states Pillai's, Erdős's, Maier and Pomerance's and Ford's results as solved variants, without Lean proofs.)

Is it an asymptotic formula? (ours, with seat O) Part (ii) is partly a question of taste, so here is what the formula contains. The scale is explicit, and we recomputed it from the definitions: ρ = 0.5425985860984710…, λ = 0.6113854845504703…, γ = 0.3234575341913807…, and the paper's C₀ = 1/(2λ) = 0.8178146400836… and D₀ = (1 + log(λ/γ))/λ − 1/2 = 2.1769687435594…, which match Ford's constants (seat O, computing separately, found agreement with Ford's own formula for D to 60 digits). The renewal sequence behaves as Ford's Lemma 3.7 says: g_jρ^j → γ, to 15 digits by j = 100. And log G_m minus Ford's exponent stays between −1.92 and −0.74 at our 60 sample points from B = log log x = 10 to B = 10^500.75 (m up to 1,874), consistent with the scale being Ford's up to a bounded factor, which seat O's limit E_∞ below proves. The coefficient is another matter. A_H is built from finitely many tail data, but its tail primes Q_h must satisfy log log Q_h ≈ α_s·h·ρ^−h with α_s ≥ λ, so already at h = 3 they exceed 10^13,000. For H ≤ 15 every witness set is empty (P = ⌊log log H⌋ = 0 would need log log Q₀ = 0, so A_H = 0), and at H = 16 the largest tail prime needs log log Q between about 7.9·10⁴ and 1.8·10⁵. The theorem gives no rate for A_H → A. Evaluating A_H at any H where the theorem applies would need primes of more than 13,000 digits, and the paper does not try: no numerical value of A is known. What the theorem does pin down is the shape of A, and the paper does not say so. We noticed the first half of this and seat O the rest; the argument is short. G_m varies continuously with x except where m increases by one, and there it jumps: G_m+1/G_m = B/((m+1)g_m+1) → λ/γ = 1.8901568828…; we computed 2.018 at m = 100, 1.910 at m = 1,000 and 1.901 at m = 2,000, with the error shrinking like (log m)/m. Between steps, a dilation x → cx moves the phase θ by only about log c/(λ·B·log x). Because V is monotone and V(cx)/V(x) → c, the convergence is uniform for c in [1, 2] (the uniform convergence theorem for regularly varying functions, which is elementary for monotone V). Comparing V(x) with V(cx) through Theorem 2.1 then forces A(1; ·) to be continuous on [0, 1), with A(1; 1⁻) = (λ/γ)·A(1; 0) ≈ 1.89·A(1; 0). In particular A is not constant. Seat O found the explicit limit of the gap to Ford's exponent: log G_m − [C₀(log₃x − log₄x)² + D₀log₃x − (D₀ + 1/2 − 2C₀)log₄x] → E_∞(θ) = θ(log(γ/λ) + λ/2) − λθ²/2 − ½log(2π/λ) − log K, with K = Π_i≥1 g_iρⁱ/γ = 0.61788…, which falls from −0.683 to −1.320 across a period and jumps back by log(λ/γ) at each step. Our own code reproduces it: K = 0.61788133, and at log B = 300, 600 and 1,000 (three phases each) the gap between the two sides is about −0.09, −0.056 and −0.039 at the middle phase, shrinking like (log log B)²/log B as O's Stirling estimate predicts. Putting the two together, Theorem 2.1's two conclusions can be restated as

V(x) = (x/log x) · exp{ C₀(log₃x − log₄x)² + D₀ log₃x − (D₀ + 1/2 − 2C₀) log₄x } · ( Φ(θ) + o(1) ),
       θ = fractional part of 2C₀(log₃x − log₄x),

with Φ = e^E∞·A(1; ·) positive, continuous and 1-periodic. So OpenAI's theorem replaces the O(1) in Ford's exponent by log Φ(θ) + o(1), a continuous periodic function of 2C₀(log₃x − log₄x). Whether Φ is constant, which would make V(x) asymptotic to a constant times Ford's expression, the theorem does not say, and nothing computable here can say. Formal Conjectures' decision to keep part (ii) open is defensible; so is calling Theorem 2.1 an answer. In our labels this paragraph is (b): rigorous given Theorem 2.1, the paper's (3.5) (g_jρ^j = γ + O(ρ^j), from Ford's Lemma 3.7), the uniform convergence theorem for regularly varying functions, and Stirling's formula, and checked numerically where it can be.

Least preimages and seeds (ours, computational). Theorem 2.2 turns Erdős's question in [Er79e] into a question about seeds, so we computed the least preimage ℓ(d) of every totient d ≤ 10⁸ in two independent ways. One is a depth-first search over prime-power factorizations, which visits every n with φ(n) ≤ 10⁹ and keeps the smallest n for each value. The other sieves φ(n) for every n ≤ 6.6·10⁸. That is enough: n/φ(n) ≤ 6.34 for every n ≤ 10¹⁰ (the largest value below 6.6·10⁸, 6.11, is at 2·3·5·⋯·23), and every larger n has φ(n) > 10⁹ by Rosser and Schoenfeld's bound. The two arrays of 10⁸ least preimages are byte-identical (same SHA-256; the 800 MB files are not in the bundle, their hashes are). A third route, the classical divisor recursion for inverting φ, reproduces every least preimage quoted here and all 10,000 terms of OEIS A049283, the table of ℓ(n) (logged in the bundle's check_external.out). Ford's seed, the one the paper uses for k = 2 (Remark 7.4), is d = 2¹⁸·257; we get ℓ(d) = 135,268,352 = 2¹¹·257², the value OpenAI's Lean proves (seed_least_preimage), ratio 257/128. It is far from the smallest. The smallest totient with ℓ(d) > 2d is d = 5,888 = 2⁸·23, with ℓ(5,888) = 11,985 = 3·5·17·47 (ratio 2.0355), and there are 133 such d up to 10⁸; seat T found the same seed independently. The records of ℓ(d)/d are 1.5 at d = 2, 1.875 at 8, 1.9922 at 128, 2.0355 at 5,888, and 2.0414 at 2,037,248 = 2⁹·23·173 (ℓ = 3·5·17·47·347), the largest up to 10⁸. Above 10⁸ the only totient with ratio over 2.0414 is 387,383,296 = 2¹⁶·23·257 (ℓ = 791,597,265 = 3·5·17·47·257², ratio 2.0434), the largest below 10⁹. To reach 10⁹ we ran the depth-first search again, this time marking, for thresholds t = 2.0414, 2.5 and 3, every totient that has a preimage n ≤ t·φ(n); a totient left unmarked has ℓ(d) > t·d. Above 10⁸ this is one algorithm, not two. The controls: on [1, 10⁸] the same search at t = 2 leaves exactly the 133 seeds above, and at t = 2.04 exactly the one record. At t = 2.5 nothing is left unmarked: every totient below 10⁹ has a preimage at most 2.5 times itself. So no seed for k = 3 exists below 10⁹, and N_k(x) = 0 for every k ≥ 3 and x ≤ 10⁹. Whether one exists at all (whether sup ℓ(d)/d > 3) is the first open instance of Erdős's question whether ℓ(d)/d is unbounded, which the paper leaves open and which stays open; the data say only that the ratio, if it grows, grows very slowly. The record least preimages are built from 3, 5, 17 and 257 (four of the five known Fermat primes) together with 47 = 2·23 + 1 and, once, 347 = 2·173 + 1. None of this is new in kind: OEIS A118700, the odd n with 2φ(n) < n and no smaller even preimage of φ(n), already contains 11,985 as its second term; we did not find the seeds or the records of ℓ(d)/d listed as such, but our search of the OEIS was not exhaustive. The companion counts at small x: N₁(x)/V(x) is 0.0906, 0.0909 and 0.0914 at x = 10⁶, 10⁷ and 10⁸, and N₂(10⁸) = 2, out of 15,037,909 totients. Theorem 2.2 says N₂(x)/V(x) is eventually bounded below by a positive constant, and nothing at this range tests that.

The counts (ours). None of these values is new: Ford's 1998 paper tabulates V(x) up to 5·10⁸ and Zeraoulia's computation reaches 10¹⁰. We recomputed them as an instrument check on the rest. The depth-first search visits all 1,943,603,114 integers n with φ(n) ≤ 10⁹; the classical density of such n, ζ(2)ζ(3)/ζ(6) ≈ 1.94360, predicts 1.94360·10⁹. Up to 10⁸ the φ-sieve, a separate algorithm, gives the same set of totients bit for bit. Between 10⁸ and 10⁹ there is one route, checked against outside tables. Our counts match all 10,000 terms of OEIS A264810 (V(n) for n ≤ 10⁴), all seven values in Ford's table (checked by seat R), every value of Zeraoulia's table that our range reaches (V(x) for x from 10³ to 10⁹, V(2x) for x up to 10⁸), and all sixteen values V(2¹⁰), …, V(2²⁵) in our July report.

        x          V(x)        V(2x)/V(x)
      10⁶       180,184         1.938557
      10⁷     1,634,372         1.947869
      10⁸    15,037,909         1.954737
  5·10⁸      71,399,658         1.958664
      10⁹   139,847,905              —

Zeraoulia's table, which goes to 10¹⁰, has V(2x)/V(x) = 1.960042 at 10⁹ and 1.963032 at 5·10⁹: over this range the ratio creeps towards 2, with 2 − V(2x)/V(x) close to 0.83/log x. That is no evidence for the theorem either way. At every x anyone can count, m = 1 (at x = 10¹⁰, (log B − log log B)/λ = 1.65), and the proof needs m > H with H large (at least 16, because for H ≤ 15, P = ⌊log log H⌋ = 0 and no tail witness exists (it would need log log Q₀ = 0), so A_H = 0). m first reaches 16 when log log log x = 12.29, that is, at x = exp(exp(217,736)).

The reading. The main seat (Claude Opus 5.5, like every seat here) read the definitions and Theorem 2.1 (§2), the Ford inputs (§3.1), the regular-variation argument (Proposition 6.1 and Corollary 6.2) and the least-preimage section (§7), checked the Lean statement against §2, and computed what is in the numerical paragraphs. Two hostile referee seats (separately briefed AI readers), each told to refute the paper and to quote what it objected to, read §§2–7 line by line between them, overlapping the main seat's reading. Both returned HOLDS AS READ: no false step and no unjustified step. They run on the same model as the main seat, so they are correlated readers, not independent ones. Seat O took §§2, 3 and 6. It recomputed the constants to 60 digits and re-derived every displayed identity in §2.1 and Lemmas 3.4–3.7 of §3 (the Dirichlet-distribution volume of Ford's simplex, the slice bounds, the Rankin step). It checked the paper's uses of Ford's Theorems 10 and 16 against the rendered pages of Ford's paper. There the text extraction garbles Ford's "i/(3L₀)" so that the split between Theorem 10(a) and 10(b) appears reversed; the rendered page shows the paper has it right. Proposition 6.1 counts the largest prime by the prime number theorem with all other data taken at x, so Corollary 6.2 (V(cx)/V(x) → c) never uses the coefficient A; it does rest on the coverage and collision results (Propositions 3.3, 3.8 and 5.1) and on (3.4). The normalization of the coefficient in (2.8) matches what §6.3 derives. Seat T took §§4, 5 and 7. It checked the sieve bound (4.3) word for word against Ford's sieve notes, every inequality of the comparison estimate (Proposition 4.2, with the exponent identity tested numerically on 2,000 random instances), and the collision count of Proposition 5.1. It tried to build collisions the argument misses: prefixes differing in many primes, equal primes in shifted positions, two shifts p − 1 and q − 1 with the same largest prime factor, two shifts on one side sharing a large prime. Each is handled by the comparison estimate or excluded by the paper's "good" conditions. It checked Lemma 7.2 against Ford's construction (pp. 24–26 and 39 of his paper): the whole inverse fibre {bd₁, …, bd_κ} survives on at least half of Ford's set, as the lemma uses it. Its main remark about the sources: the paper requires the whole product of shifted primes to be squarefree, not just each shift, and says that per-shift squarefreeness would not suffice. Ford's own Lemma 5.1, from which this comparison is adapted, assumes only that no p_i − 1 is divisible by r² for a large prime r, and then writes "by assumption (1), t is squarefree" about a product over several shifts, which does not follow when one prime divides two different shifts. We read that page and agree that the sentence does not follow as written. The slack looks ample (squares of primes this large cost little), and we have not written out a repair, so we report it as a gap in the wording of Ford's step, not an error in his theorem. The paper avoids the issue. Exposition notes, none load-bearing. The paper's "explicit" is definitional (seat O). Theorem 2.1's two conclusions force A to be continuous with a fixed ratio between its values at the two ends of the phase interval, which the paper never says (above). Remark 7.4 establishes k = 2 with Ford's seed 2¹⁸·257, through the fact that all its preimages are divisible by 8; much smaller seeds exist. Definition 3.1 writes S ≥ e^e where Ford writes S ≥ 2, which is immaterial. A fourth seat, R, was briefed to refute our own claims as stated in its brief (the λ/γ bound in the form sup A/inf A ≥ λ/γ, the counts, the bridge), and returned HOLDS AS READ. It re-derived the λ/γ argument and its direction (A drops by a factor of about 1.89 as the phase wraps), and confirmed that direction separately from the definition (2.8). It reproduced our counts up to 10⁷ with an independent brute force, recompiled our C programs and found their outputs at 10⁷ bit-identical to it, re-found the 133 seeds below 10⁸ and ℓ(387,383,296) = 791,597,265 by another method, and found no overflow, off-by-one or rounding problem; double-precision rounding in the threshold search could only create a false seed, never hide a real one. It checked the bridge against Formal Conjectures' file at 32ac619d and at main (byte-identical) and found that the OpenAI commit FC links to has no diff against ours in these files. Its main fixes are applied: our counts are not new, above 10⁸ they rest on one algorithm, and the OEIS has related tables. It advised stating the end-of-interval relation only as sup A/inf A ≥ λ/γ, since R was not asked to check continuity. We state the stronger form because the uniform convergence in c gives continuity (seat O's argument, which the main seat re-derived); R did not check that step.

Sources, priority and the world. The world seat (a separately briefed AI reader with web access) checked the sources and the priority record. It returned GAP, for the paper's framing only: every cited place says what the paper says, but the paper's novelty claim leaves out an earlier public proof of part (i). Priority. conjectures.io, a bounty site running on the Bittensor network, lists a Lean proof of exactly Formal Conjectures' erdos_416.parts.i, V(2x)/V(x) → 2, by a solver called JenW1N: "Verified 14 Sept 2026", "Certified 16 Sept 2026", 64,775 lines, permitted axioms propext, Quot.sound and Classical.choice. The seat downloaded the source today; its SHA-256 matches the one the site publishes. Thomas Bloom posted it on the #416 proof-claims tab on 27 September, noting that he had not verified it. OpenAI's preprint is dated 25 September, and the repository and the paper's first commit appeared on 6 October; the text we reviewed is byte-identical to that first commit. So the doubling limit had a machine-verified proof on 14 September, published on conjectures.io on 16 September: nine days before the paper's date and three weeks before its release. Who proved it first privately cannot be told from public data; FC's docstring says an internal OpenAI model proved it in September. The paper does not mention it, nor Rafik Zeraoulia's partial result of 29 July (below), and Formal Conjectures' PR #6898, which marked parts.i solved on 11 October, credits only OpenAI. We have not replayed the conjectures.io proof; its review relied on the site's own Lean check and claims no further replay or line-by-line audit, and its prose exposition now returns 404. Judging from the docstrings in the conjectures.io Lean, that proof takes the same route, counting the largest prime over a Ford-type structure and bounding collisions with a sieve, for c = 2 only and with no limiting coefficient. What the paper has first, as far as anyone found, is every c > 0, the asymptotic equivalent and the least-preimage theorem. Zeraoulia. His repository (github.com/rafikmath15/fixed-scale-totient-limit-points, 29 July) claims a proof, which we have not checked, that for every c > 1, lim inf |V(cn)/V(n) − c| = 0 and that the cluster set of V(cx)/V(x) is a closed interval containing c, and says plainly that this is not convergence. Its table, computed to 10¹⁰, agrees with ours at every point both have. Sources. The seat checked each citation at the cited place, rendering pages where text extraction failed, and all hold. They include Ford's Theorems 1, 2, 4, 10 and 16, his Lemmas 2.6, 3.4 and 3.7, his equations (5.10)–(5.19) and the seed on his p. 39. They include Erdős and Hall's question (Mathematika 23, 1976, p. 3: "is it true that, for every c > 1, lim V(cx)/V(x) = c?"). Erdős in Astérisque 61 (1979), p. 80, asks both the dilation question and the least-preimage one, and adds "It is not certain that there is a genuine asymptotic formula". Erdős 1995, §I.9, asks whether ℓ(d)/d can tend to infinity. Maier and Pomerance's constant, Pomerance's (1.4), Pollack, Pomerance and Treviño's Lemma 4.1 and Ford's sieve notes also check out. One defect is the paper's: the DOI it gives for Erdős 1995 (copied from the journal's own page) does not resolve. One is the source's: Ford's p. 15 says "A_i > 4 for all i" where only the normalized A_i/g_i > 4 is true (minimum 4.003), a slip the conjectures.io Lean also flags; the paper uses only the lemma's conclusion. Erdős #51. Erdős's question whether ℓ(d)/d is unbounded, the hinge of Theorem 2.2 for k ≥ 3, is erdosproblems.com #51, open there and in Formal Conjectures; the paper cites it as [5, §I.9] but not by number. On that problem's thread Terence Tao wrote (10 August 2025) that the answer is most likely negative, ℓ(d)/d bounded: a minimal preimage with too many prime factors should allow a swap that lowers it. Vjeko Kovac refined this to small prime factors, noting that products of Fermat primes such as 3·5·17·257 have many prime factors yet n/φ(n) < 2. Our records use 3, 5 and 17 together with 47, and once 347 and once 257²; the excess over 2 comes from the factors that are not Fermat primes. The records grow from 2.0355 to 2.0434 between 5,888 and 3.9·10⁸. Formal Conjectures. Part (ii) stays open there for a stated practical reason: PR #6898 says "the main term needs many auxiliary definitions", and issue #6907 counts about 25. No one there has questioned the mathematics. (As a bare Lean statement, FC's parts.ii would be satisfied by taking the answer to be V itself; it is a question-value item that people, not the checker, judge.) Tao's erdosproblems database still lists #416 as open, last updated 31 August 2025. Other claims and criticism. None found. The search covered arXiv (rate-limited, so partial), the web, Formal Conjectures' issues and erdosproblems.com, whose page now says a formalised proof of V(cx)/V(x) → c is available and links OpenAI's comparator statement file.

What this entry is. A referee report on someone else's proof. The theorem, its proof and its Lean formalization are OpenAI's, and part (i) was first proved publicly, in Lean, on conjectures.io. Ours: the replay and its controls, the bridge to Formal Conjectures' statements and its controls, the readings, the recomputed constants and the scale check, the remark that A cannot be constant, and the counts and seed search. Our labels: (b) means rigorous modulo cited results, (d) means computer-assisted. The proof as printed is (b), rigorous modulo cited results of Ford: Theorems 1, 10 and 16; Lemmas 2.6, 3.4 and 3.7 and Corollary 3.5; the construction in his proof of Theorem 2; and the sieve bound of his lecture notes (Theorem 2.5). Our seats checked these at the cited places but did not re-prove them. The Lean statement, which proves what it needs without citing Ford, is (d): every OpenAI, PNT+ and LeanArchitect module was kernel-checked here by compiling it, and Mathlib's cached files by leanchecker --fresh (exit 0). The consequences for A (continuity, the ratio at the ends, so A is not constant) are (b), with the inputs listed in that paragraph. The counts and seeds are (d): up to 10⁸ every number is reproduced by a second, independent method; above 10⁸ they rest on one algorithm, checked against Ford's and Zeraoulia's tables. Every seat and the main session were served by Claude Opus 5.5; per-seat counts, and a zero count of any other model, are in the bundle's seats/MODEL_RECEIPTS.txt.