Formally verified AI-assisted

Erdős Problem 408: an unconditional normal order for the number of totient iterations

A Lean-checked proof that the least $k$ with $\varphi_k(n) = 1$ has normal order $\alpha \log n$ for a constant $1/\log 3 \le \alpha \le 1/\log 2$ , answering the first two questions of Erdős Problem 408 without the Elliott-Halberstam hypothesis a 1990 proof needed, by building on OpenAI's unrefereed zero-free half-plane and shifted-prime results.

Lab: Plasma AI
Model: Claude Opus 5.5 (Lean formalization); the argument is credited to Plasma AI without naming a model
Field: Mathematics
Date: 2026-10-19
Human collaborators: Jacob Parish
Problem posed: 1980 · open 46 yrs

Sources

Original work

GitHubplasma-ai/erdos-408, the Lean development↗GitHubPlasma AI: The normal order of the number of iterations of Euler's function (PDF)↗

What was found

Let $f(n)$ be the least $k \ge 1$ with $\varphi_k(n) = 1$ . Pillai showed in 1929 that $f(n)$ lies between about $\log n/\log 3$ and $\log n/\log 2$ , and Erdős, Granville, Pomerance and Spiro proved in 1990 that it has normal order $\alpha \log n$ conditionally on a form of the Elliott-Halberstam conjecture. This development removes the condition, with mean-square error $O(x (\log x)^2/(\log \log x)^5)$ , so $f(n)/\log n$ tends to $\alpha$ on a set of density one and its distribution function is the point mass at $\alpha$ . The inputs that replace Elliott-Halberstam are OpenAI's zero-free half-plane $\operatorname{Re} s > 7/8$ for Dirichlet L-functions and the transference machinery of two OpenAI shifted-prime preprints of 24 September 2026, extended here. The Lean proofs of the half-plane, and Yao Xu's formalization of one of those preprints, are vendored and build with the project, so neither is assumed. The third, open-ended question of the problem is not formalized.

Novelty check

On 2026-10-20 erdosproblems.com listed Problem 408 as open, citing only the conditional 1990 result, with no proof claims, and Formal Conjectures lists both questions as open. The paper says that to its authors' knowledge the unconditional normal order has not been recorded before. A web search on 2026-10-20 found no competing claim.

Caveats and known objections

Graded formal on the Palomar registration and on the statement: the definition of $f$ and the statements erdos_408.parts.i and parts.ii are Formal Conjectures' at commit 7db2ea3b91, except that its Set.HasDensity is written out in place, and with its default reference set of all naturals that definition reduces to the inlined one. The normal_order_rate theorem with its explicit rate is the authors' own statement, in Mathlib terms. The grade certifies the theorems, not the paper, which is self-published and unrefereed; the repository's review status is self-assessed and no mathematician is on record as having read it. The mathematics leans heavily on OpenAI's quasi-Riemann hypothesis and Poisson-Dirichlet preprints, produced by an unreleased model and unrefereed; their Lean proofs build here, so the theorems stand on them formally, but nobody outside OpenAI has read their exposition either. Autonomy is graded ai-assisted on what is disclosed: unlike its two sibling repositories, this one credits the argument to Plasma AI without saying whether models found it, and records only that Claude Opus 5.5 led the formalization, with parallel subagents writing proofs. The grade should be revisited if the discovery is disclosed.

Independent checks

whataifound.org (statement comparison): Compared Challenge.lean at commit 4ea44bf9 with Formal Conjectures' ErdosProblems/408.lean at 7db2ea3b: the definition of f is identical, and parts.i and parts.ii differ only in writing Set.HasDensity out as a ratio of counts below b, which is Formal Conjectures' own definition with its default reference set of all naturals. · link ↗

Machine-checked elsewhere

PalomarPALOMAR-2026-10-19-000009

plasma-ai/erdos-408 at 4ea44bf911f8 · checked 2026-10-19

ProvedErdos408.normal_order_rateErdos408.erdos_408.parts.iErdos408.erdos_408.parts.ii

A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.

Permitted axioms are exactly propext, Quot.sound and Classical.choice. parts.i and parts.ii are Formal Conjectures' statements; normal_order_rate is the authors' own.

Disagree with these grades?

Bring a citation: a grade moves on evidence, not on argument.

Challenge this grade Submit a check

Or on GitHub: submit a check challenge the grade send a correction or send a pull request

Entry history (1 event)

2026-10-20AddedEntered the registry graded Formally verified and AI-assisted.

Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.

Graded formally verified for verification and ai-assisted for autonomy. What these mean.

Cite this entry

Plain text

whataifound.org. (2026). Erdős Problem 408: an unconditional normal order for the number of totient iterations. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-19-erdos-408-iterated-totient

BibTeX

@misc{whataifound-plasmaai-2026-totient,
  title        = {Erdős Problem 408: an unconditional normal order for the number of totient iterations},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by Plasma AI. Verification: Formally verified. Autonomy: AI-assisted.},
  url          = {https://whataifound.org/finding/2026-10-19-erdos-408-iterated-totient}
}

Related findings

Formally verifiedNo zeros of any Dedekind zeta function with real part above 31/32, machine-checked in LeanAxiom Math · 2026-10-12 Formally verifiedErdős Problem 173: a two-coloring of the plane misses at most one triangle, which is equilateralPlasma AI · 2026-10-19 ClaimedLambert series values, including the Erdős-Borwein constant, are not quadratic irrationalsIndependent · 2026-10-08

number-theory analytic-number-theory erdos-problems lean formalization argument

← All mathematics findings in the registry