Erdős Problem 694

Reference: erdosproblems.com/694

theorem erdos_694 (max min : ℕ → ℕ) (hmax : ∀ (n : ℕ), IsGreatest (Nat.totient ⁻¹' {n}) (max n)) (hmin : ∀ (n : ℕ), IsLeast (Nat.totient ⁻¹' {n}) (min n)) (x : ℕ) : IsGreatest {x_1 : ℚ | ∃ (n : ℕ) (_ : n ≤ x), ↑(max n) / ↑(min n) = x_1} sorry

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)}. $$

theorem erdos_694.variants.carmichael : (∃ n > 0, ∃! m : ℕ, m.totient = n) ↔ sorry

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 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$.