---

Claim. Theorem 1.1 of Plasma AI, The normal order of the number of iterations of Euler's function, preprint (2026): there is a constant $\alpha$ with $1/\log3\le\alpha\le1/\log2$ such that $\sum_{n\le x}(f(n)-\alpha\log n)^2\ll x(\log x)^2/(\log\log x)^5$, and the $n\le x$ with $|f(n)-\alpha\log n|>\log n/\log\log n$ number $O(x/(\log\log x)^3+\sqrt x)$. Hence $f(n)/\log n\to\alpha$ on a set of natural density one: $f(n)/\log n$ has a distribution function, the unit step at $\alpha$, and is almost always constant in the normal-order sense of the Formulation on the problem page. The paper counts iterations from $\varphi_0(n)=n$, so its $f(1)=0$ where the problem page's $f(1)=1$; the two agree for $n\ge2$, and no density changes. The value of $\alpha$ is not determined. The proof runs the moment method of Erdős, Granville, Pomerance and Spiro without their Elliott--Halberstam-type hypothesis, which it replaces by a quantitative estimate for tuples of prime factors of $p-1$ (its Theorem 2.1), extending Theorem 7.1 of OpenAI's Poisson--Dirichlet manuscript and resting on OpenAI's zero-free half-plane $\operatorname{Re}s>7/8$ and its weighted-dilation-graph results. The source card plasma_ai_2026_normal_order_number_iterations_euler_s_function digests the paper and the formalization.

Covers. The first two questions, the parts distribution and constant. The third question, which is open-ended and not a part, is not covered by the claim; the paper's remark on it, a consequence of Ford, Konyagin and Luca (2010, Theorem 5), is recorded on the source card.

Formalization. The repository plasma-ai/erdos-408 formalizes Theorem 1.1 in Lean 4 (v4.35.0, Mathlib v4.35.0). Challenge.lean states it as Erdos408.normal_order_rate, together with formal-conjectures' statements of the first two questions, erdos_408.parts.i and erdos_408.parts.ii at its commit of 2026-10-14, with f copied verbatim and the density inlined; Solution.lean proves the three, and comparator.json permits only propext, Quot.sound and Classical.choice. The repository's formalization.yaml names Jacob Parish as the formalization's author, records that it was written with Claude Code, and gives its review status as self-assessed, with a Comparator check run on macOS without the landrun sandbox.

Acceptance. Formalized. This corpus rebuilt the formalization, held as the repository's tree at 5b02bf9 without its paper/ folder, at its own pinned toolchain, leanprover/lean4:v4.35.0 with Mathlib at v4.35.0, in a sandbox with no network. Comparator, run before anything else built the solution, accepted the three theorems against Challenge.lean. The kernel then replayed, from an empty environment, every declaration each of the three depends on, Lean core, Mathlib and the vendored libraries included, and accepted them all. Each theorem's type, and every constant its statement reaches, are identical in Challenge.lean and Solution.lean, and each depends only on propext, Classical.choice and Quot.sound (the replay receipt, 2026-10-14). The graded fresh-context review of the statements against the problem page and the preprint found all three faithful, with partial coverage, since the third question is not formalized. Acceptance rests on the replay and that review, and covers the parts distribution and constant. The preprint is unrefereed, and no named mathematician has reviewed the proof. The source's own attestations, the author's sign-off and the formalization's Comparator run, are reported, not counted.

Depends on. The claim rests on the cited preprint and its formalization: its Theorem 1.1, with the Poisson--Dirichlet manuscript's Theorem 7.1 and the zero-free half-plane as inputs.