Double x, double V?
An asymptotic formula for the number of totients
Covers result 024 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
4:20. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
Euler’s totient φ(n) counts the numbers up to n that share no factor with n except 1. Its values skip every odd number above 1 and some even numbers, like 14 and 26. Let V(x) be the number of distinct values up to x: V(10) = 6, V(106) = 180,184 and V(107) = 1,634,372.
Result 024 (39 pages) claims an asymptotic formula, V(x) ~ (x/log x)·Gm·A(θ). Here (x/log x)Gm is the scale found by Ford, and θ is a phase that moves with log log log x. A is a uniform limit of explicit formulas built from finite arithmetic data, and it stays between two positive constants. Separately, by counting the largest prime factor of a preimage, the paper claims that V(cx)/V(x) → c for every fixed c > 0, answering a question of Erdős and Hall (Erdős problem #416). It also gives asymptotics for totients counted by the size of their smallest preimage.
What it doesn’t claim
The coefficient A is a limit, not a computed number. The paper doesn’t say whether A really varies with the phase, and it gives no rate of convergence. The phase is about 0.64 at x = 107 and completes its turn only around x ≈ 10213. Whether the smallest preimage of a value can be arbitrarily large compared with the value is left open.
Where it stands
- Posted as a preprint
- OpenAI, dated September 25, 2026, released October 6; 39 pages
- Peer reviewed
- Not yet
- Checked in Lean
- By OpenAI (scope note); we have not run the check
Last checked October 19, 2026. The claim has not been withdrawn, and we found no public response to it; erdosproblems.com still lists problem #416, which asks both whether V(2x)/V(x) → 2 and for an asymptotic formula, as open. OpenAI’s Lean statements (the main theorems and the zero case) match Theorems 2.1 and 2.2. Following their imports gives about 800 files and 73,000 lines, not counting Mathlib and the prime number theorem library they use, with no unfinished proofs (sorry) in OpenAI’s files. Ford’s structure theorems are proved there, not assumed. The result is not listed in OpenAI’s formalization catalog.
What was known
- Since φ(p) = p − 1, V(x) is at least about x/log x. Pillai (1929) proved the values have density zero.
- Erdős (1935), Erdős and Hall (1976) and Pomerance (1986) brought the bounds onto the same scale, and Maier and Pomerance (1988) found V(x) = (x/log x)·exp{(C0 + o(1))(log log log x)2}, C0 = 0.8178….
- Ford (1998) found V(x) up to a bounded factor and proved V(cx) − V(x) ≍ V(x), so the ratio V(cx)/V(x) stays between two constants above 1 for c > 1.
How the proof goes
- Structure. By Ford’s structure theorems, almost every value has all its preimages of a typical shape: prime factors p0 > p1 > … whose log log sizes sit near a fixed decreasing pattern.
- Prefix and tail. A long prefix of large primes is counted by volume, as a region of a simplex. A short tail of small primes is kept exactly, because different tails can give the same totient; inclusion–exclusion over those finitely many tails produces the coefficient.
- Collisions. Comparing products of shifted primes (p − 1)(q − 1)… in the layered method of Maier, Pomerance and Ford, with each sieve step handling two or three linear forms, shows that different prefixes rarely give the same value.
- Scaling. Counting the largest prime p with (p − 1)·d ≤ x is like counting primes up to x/d, which scales by c when x does. Done uniformly, this gives V(cx)/V(x) → c; identifying the mass with A gives the formula.
The numbers in the video
- A short Python script computes φ(n) for every n up to 62 million, which gives every totient value up to 107. It finds V(10k) = 6, 38, 291, 2,374, 20,254, 180,184 and 1,634,372 for k = 1, …, 7.
- The ratio V(x)/(x/log x) is 2.19, 2.33, 2.49 and 2.63 at 104, …, 107. The ratio V(2x)/V(x) is 1.890, 1.925, 1.939 and 1.945 at x = 104, 105, 106 and 5·106.
- The script also reproduces C0 = 0.8178146 and D0 = 2.1769687, and the phase at 107.
Read the source
- An asymptotic formula for the number of totients (PDF), dated September 25, 2026 (39 pages).
- The Lean statements: TotientAsymptotic.lean and TotientCompanionZero.lean, and OpenAI’s scope note.
- Kevin Ford, The distribution of totients, and Erdős problem #416.
- The collection’s catalog, where this is result 024.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00Missing values
Euler’s totient, φ(n), counts the numbers up to n that share no factor with n except one. φ(9) is six, and φ(10) is four. As n runs through the integers, φ(n) hits some values many times, and skips others completely. Every odd number above one is skipped, and so are some even numbers, like 14 and 26. Let V(x) count the distinct values up to x. Up to ten there are six. Up to a million, about 180,000. Up to 10 million, about 1.63 million. Result 024 in OpenAI’s math repository claims an asymptotic formula for V(x), and answers a question of Erdős and Hall.
0:44How many values?
φ of a prime p is p − 1, so every prime gives a value: V(x) is at least about x/log x. In 1929, S. S. Pillai showed that the values still have density zero. Over the next 60 years, Erdős, Hall, Pomerance and Maier narrowed the growth to x/log x, times a factor like e to the power of a constant times (log log log x)². In 1998, Kevin Ford pinned down the size, up to a bounded factor. Up to 10 million, V(x) is about 2.6 times x/log x, and that ratio keeps creeping up, extremely slowly. Erdős and Hall asked a sharper question. If you double x, does V(x) double, in the limit? More generally, does V(cx)/V(x) tend to c? Ford showed the ratio stays between two constants above one, but not where it goes. Up to 10 million, doubling x multiplies V by about 1.95.
1:43The claim
The preprint, 39 pages, dated September 25, claims an asymptotic formula: V(x) is Ford’s scale, times a coefficient A of a slowly turning phase, theta. A is a limit of formulas built from finite arithmetic data, and stays between two positive constants. The phase moves with log log log x. At 10 million it sits at about 0.64, and it doesn’t complete its turn until x is around 10^213. Separately, by counting the largest prime factor, the paper proves that V(cx)/V(x) tends to c, for every fixed c. The paper’s answer to Erdős and Hall is yes. It also counts totients by the size of their smallest preimage. OpenAI published a Lean proof of these statements, about 800 files and 73,000 lines, not counting Mathlib and the libraries it uses. We haven’t run the check.
2:41How the proof goes
A typical value comes from an n whose prime factors, in decreasing order, shrink in a regular pattern: Ford showed where their log log sizes sit. The proof splits these primes into a long prefix and a short tail of small primes. The prefix is counted by volume, as a region of a simplex. The tail is kept exactly, because different tails can give the same value. Inclusion-exclusion over those finitely many tails produces the coefficient A. The danger is collisions: different prefixes giving the same value. Comparing products of shifted primes, like (p − 1)(q − 1), in the layered method of Maier, Pomerance and Ford, shows they are rare. Then the largest prime does the scaling. Fix the rest of n, with totient d. Counting the largest prime p with (p − 1)·d below x is like counting primes up to x/d, and multiplying x by c multiplies that count by c, in the limit. The paper makes this work for all the pieces at once.
3:47Where it stands
This is a preprint, not peer reviewed, and we haven’t run the Lean check. The coefficient A is a limit, not a number you can look up, and the paper doesn’t say whether it really varies with the phase. No rate is claimed. Whether the smallest preimage of a value can be arbitrarily large compared with the value stays open. Totient values thin out in a way that took most of a century to measure. If the proof holds, multiplying x by c multiplies their count by c, in the limit.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.