Erdős Problem 694

Reference: erdosproblems.com/694

theorem Erdos694.erdos_694 (fmax fmin : ℕ → ℕ) : (∀ (n : ℕ), IsGreatest (Nat.totient ⁻¹' {n}) (fmax n)) → (∀ (n : ℕ), IsLeast (Nat.totient ⁻¹' {n}) (fmin n)) → ∃ (o : ℕ → ℝ), Filter.Tendsto o Filter.atTop (nhds 0) ∧ ∀ (x : ℕ), sSup {x_1 : ℝ | ∃ (n : ℕ) (_ : n ≤ x) (_ : ∃ (m : ℕ), m.totient = n), ↑(fmax n) / ↑(fmin n) = x_1} = (Real.exp Real.eulerMascheroniConstant + o x) * Real.log (Real.log ↑x)

Let $f_\max(n)$ be the largest $m$ such that $\phi(m) = n$, and $f_\min(n)$ be the smallest such $m$, where $\phi$ is Euler's totient function. Investigate $$ \max_{n\leq x}\frac{f_\max(n)}{f_\min(n)}. $$

GPT-5.5 Pro (prompted by Price) has proved (see also the comments for a summary) that $$ \max_{n\leq x}\frac{f_{\max}(n)}{f_{\min}(n)}=(e^\gamma+o(1))\log\log x. $$

A Lean formalisation of the reduction exists, conditional on Mertens' product theorem and Linnik's theorem; see the formal proof.

theorem Erdos694.erdos_694.variants.carmichael : True ↔ ∃ n > 0, ∃! m : ℕ, m.totient = n

Carmichael has asked whether there is an integer $n$ for which $\phi(m) = n$ has exactly one solution, that is $\frac{f_\max(n)}{f_\min(n)} = 1$.

theorem Erdos694.erdos_694.variants.inf_unique (h : ∃ n > 0, ∃! m : ℕ, m.totient = n) : {n : ℕ | ∃! m : ℕ, m.totient = n}.Infinite

Erdős has proved that if there exists an integer $n$ for which $\phi(m) = n$ has exactly one solution, then there must be infinitely many such $n$.