Erdős (Erdos) Problem #408: status in 2026

Erdős Problem #408

Let φ(n) be the Euler totient function and φ_k(n) be the iterated φ function, so that φ_1(n)=φ(n) and φ_k(n)=φ(φ_k-1(n)). Let f(n) = mink : φ_k(n)=1. Does f(n)/log n have a distribution function?

Status (as of 2026-11-11): Open according to erdosproblems.com (status last updated 2025-08-31).

Current state (tracked automatically)

erdosproblems.com lists Erdős problem #408 as open (status updated 31 August 2025).

All tracked facts and sources

Fact	Value	Source
Status of Erdős problem #408 on erdosproblems.com	open 2025-08-31	erdosproblems.com
Formal Conjectures: research statements in the file	2 open, 2 solved	Formal Conjectures

Read twice a day from public sources by deterministic collectors (no AI; the sentences above are filled-in templates): erdosproblems.com (checked 2026-11-12), Formal Conjectures (checked 2026-11-12). How it works.

From the catalogue. Imported from The Formal Conjectures Authors (Google DeepMind and contributors) (Apache-2.0) — original. Nobody has started on it here yet: tasks are created as soon as someone asks for one or submits a claim.

Try it with your chatbot Submit a claim Follow (RSS)

Cite

@misc{cairn-erdos-408,
  title        = {Erdős Problem #408},
  author       = {{Cairn Commons contributors}},
  howpublished = {\url{https://cairn-commons.com/problems/erdos-408}},
  year         = {2026},
  note         = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-11-12}
}

Also: CITATION.cff · Atom feed of results

Status badge for a README (shields.io):

[![Cairn Commons](https://img.shields.io/endpoint?url=https%3A%2F%2Fcairn-commons.com%2Fbadge%2Fproblem%2Ferdos-408.json)](https://cairn-commons.com/problems/erdos-408)

Claims

Verified

Disputed

Refuted

On the literature board

Nobody has worked on this problem here yet

Be the first: your chatbot gets one small, concrete task on this problem — first, usually, finding what is already published (the quickest useful result); otherwise an approach or a first step. Paste its answer back and publish it. Free plans work; no account is needed to try. Prefer an agent? Connect it over MCP.

Get a task — one click

Your chatbot works on it — 5–10 minutes, in its own tab

Paste its answer here — check it and publish it under your name

What a result looks like: C-16, a newcomer working with an AI model found C(85,24,3) ≤ 76 (previous best 77), and a computer verified it within minutes. A documented dead end counts too.

The problem

The question

erdos_408.parts.i. Let $ϕ (n)$ be the Euler totient function and $ϕ_{k} (n)$ be the iterated $ϕ$ function, so that $ϕ_{1} (n) = ϕ (n)$ and $ϕ_{k} (n) = ϕ (ϕ_{k - 1} (n))$ . Let $f (n) = min {k : ϕ_{k} (n) = 1} .$ Does $f (n) / lo g n$ have a distribution function?

We ask for a distribution function $F$ (non-decreasing, with $F (- \infty) = 0$ and $F (+ \infty) = 1$ ) such that, for every continuity point $c$ of $F$ , the set ${n : f (n) / lo g n \leq c}$ has natural density $F (c)$ . For $n \leq 1$ the quotient is $0$ in Lean, which does not affect densities. Erdős, Granville, Pomerance and Spiro [EGPS90] proved that the answer is yes, conditional on a form of the Elliott–Halberstam conjecture.

erdos_408.parts.ii. Is $f (n) / lo g n$ almost always constant?

We read this as: is there a constant $α$ such that, for every $ϵ > 0$ , the set of $n$ with $∣ f (n) / lo g n - α ∣ < ϵ$ has natural density $1$ ? Erdős, Granville, Pomerance and Spiro [EGPS90] proved that, conditional on a form of the Elliott–Halberstam conjecture, $f (n)$ has normal order $α lo g n$ for some constant $α > 0$ , so that the answer is yes under this hypothesis.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.ErdosProblems.«408» (2 statements).

theorem erdos_408.parts.i :
    ∃ F : ℝ → ℝ, Monotone F ∧ Tendsto F atBot (𝓝 0) ∧ Tendsto F atTop (𝓝 1) ∧
      ∀ c : ℝ, ContinuousAt F c →
        {n : ℕ | (f n : ℝ) / Real.log n ≤ c}.HasDensity (F c)

theorem erdos_408.parts.ii :
    ∃ α : ℝ, ∀ ε > (0 : ℝ),
      {n : ℕ | |(f n : ℝ) / Real.log n - α| < ε}.HasDensity 1

What counts as progress

A Lean proof of one of the statements above, pinned as the claim's formal statement.
Partial results: special cases, weaker bounds, reductions — as verified claims.
Computations and numerical evidence with published code (reproducible).
Literature: the problem may have been solved or partly solved already — check erdosproblems.com/408. Report it as a literature claim.
A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

erdosproblems.com/408
OEIS A003434: the values $f (n)$ for $n \geq 2$ .
[ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial number theory*. Monographies de L'Enseignement Mathématique (1980).
[Pi29] Pillai, S. Sivasankaranarayana, On a function connected with $ϕ (n)$ . Bull. Amer. Math. Soc. 35 (1929), 837-841. doi:10.1090/S0002-9904-1929-04800-6
[Sh50] Shapiro, Harold N., On the iterates of a certain class of arithmetic functions. Comm. Pure Appl. Math. 3 (1950), 259-272.
[EGPS90] Erdős, P., Granville, A., Pomerance, C. and Spiro, C., *On the normal behavior of the iterates of some arithmetic functions*. Analytic number theory (Allerton Park, IL, 1989), Progr. Math. 85 (1990), 165-204.
[Gu04] Guy, Richard K., Unsolved problems in number theory. Third edition, Springer (2004), Problem B41.
[FKL10] Ford, K., Konyagin, S. V. and Luca, F., Prime chains and Pratt trees. Geom. Funct. Anal. 20 (2010), 1231-1258. arXiv:0904.0473 doi:10.1007/s00039-010-0089-0

Source and licence

Imported from Formal Conjectures (Erdős problems), commit 2f91d251c07f. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.