An asymptotic formula for the number of totients

1 paperLean

Gives an asymptotic equivalent for the number \(V(x)\) of distinct totient values up to x, with a positive bounded phase-dependent factor determined by convergent arithmetic approximations. In particular, \(V(cx)/V(x)\to c\) for every fixed c > 0, answering Erdős and Hall’s scaling question.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

An asymptotic formula for the number of totients

OpenAI · September 25, 2026

Let \(V(x)\) count the distinct values of Euler's totient function up to x. We give an explicit asymptotic equivalent for \(V(x)\). Its coefficient is a uniform limit of functions defined from finite arithmetic data. We also prove that \(V(cx)/V(x)\to c\) as \(x\to\infty\) for every fixed c > 0, answering a question of Erdős and Hall.

Read PDF Download Source

Cite

@misc{OAI:An-asymptotic-formula-for-the-number-of-totients-September-25-2026,
  author = {{OpenAI}},
  title = {{An asymptotic formula for the number of totients}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-asymptotic-formula-for-the-number-of-totients-September-25-2026/An-asymptotic-formula-for-the-number-of-totients-September-25-2026.pdf}{OAI:An-asymptotic-formula-for-the-number-of-totients-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

An asymptotic formula for the number of totients

Scope

Let \(V(x)\) count the distinct values of Euler's totient function up to \(x\). The formalization constructs the paper's explicit positive main term from finite arithmetic approximants and proves that their ratio tends to one. In particular, \(V(cx)/V(x)\to c\) for every fixed \(c>0\), answering the Erdős–Hall regular-variation question.

The formalization also gives asymptotics for totients \(v\le x\) whose least preimage \(\ell(v)=\min\{n\ge1:\varphi(n)=v\}\) lies between \(kx\) and \((k+1)x\). The associated coefficient is positive under the stated existence condition; when no totient \(d\) satisfies \(kd<\ell(d)\), the count and coefficient are identically zero. The cases \(k=1,2\) have positive coefficients.

Comparator links

Result	Comparator statement
Totient-count asymptotics and regular variation	TotientAsymptotic.lean
Exact zero case for the companion totient counts	TotientCompanionZero.lean

Scope note on GitHub →