{"id":"palomar/PALOMAR-2026-10-19-000009","url":"https://github.com/plasma-ai/erdos-408/tree/4ea44bf911f8668aec10ec25c4b309e8ed476666","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-19-000009-v1.json","repo":"https://github.com/plasma-ai/erdos-408","tags":["math.NT","msc:11A25","msc:11N37","msc:11N64","number-theory","totient-function","formalization"],"score":0,"title":"Erdős Problem 408: distribution of iterated totient heights","trust":"high","domain":"math.NT","source":"palomar","authors":["Jacob Parish"],"reviews":0,"subject":"math.NT","summary":"A Lean proof that the least k with φ_k(n) = 1 has normal order α log n for a constant 1 / log 3 ≤ α ≤ 1 / log 2, with mean-square error O(x (log x)² / (log log x)⁵). This answers the first two questions of Erdős Problem 408. The proof formalizes extensions of Theorems 3.1 and 6.1 of OpenAI's The Poisson-Dirichlet law for prime predecessors, and uses vendored Lean proofs of the zero-free half-plane re s > 7/8 for Dirichlet L-functions (openai/math) and of the weighted dilation graph results (Yao Xu's totient-fibers-lean4).","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-19","reactions":{},"formalized":true,"formalizes":[{"title":"The normal order of the number of iterations of Euler's function","identifier":"https://github.com/plasma-ai/erdos-408/blob/main/paper/totient_iterates.pdf","relationship":"formalizes"},{"title":"On the normal behavior of the iterates of some arithmetic functions","identifier":"Analytic number theory (Allerton Park, IL, 1989), Progr. Math. 85 (1990), 165–204","relationship":"adapts"},{"title":"The Poisson-Dirichlet law for prime predecessors","identifier":"https://github.com/openai/math/blob/main/preprints/The-Poisson-Dirichlet-Law-for-Prime-Predecessors-September-24-2026/paper.pdf","relationship":"formalizes"},{"title":"PrimeNumberTheoremAnd","identifier":"https://github.com/AlexKontorovich/PrimeNumberTheoremAnd","relationship":"adapts"},{"title":"totient-fibers-lean4","identifier":"https://github.com/cadamcat/totient-fibers-lean4","relationship":"adapts"}]}