FormalConjectures/ErdosProblems/694.lean

GitHub source file

3 declarations, 3 contain sorry, 0 declared as axioms

1. theorem Erdos694.erdos_694 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 sorry line 54 source

   Source documentation

   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.

   The extrema are only required on nonempty fibres of the totient (values such as $3$ have no preimage), and the identity is asked for sufficiently large $x$: at $x = 1$ the maximum is $f_\max(1) / f_\min(1) = 2$ while $\log \log 1 = 0$.

   L4DEL explanation

   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. The extrema are only required on nonempty fibres of the totient (values such as $3$ have no preimage), and the identity is asked for sufficiently large $x$: at $x = 1$ the maximum is $f_\max(1) / f_\min(1) = 2$ while $\log \log 1 = 0$.

   Sources and attribution: Pinned Lean source (1646ca16afd6)

   depends on sorry what this means

   Statement uses: Nat, Exists, Eq, Nat.totient, IsGreatest, Set.preimage, Singleton.singleton, Set, IsLeast, Real, And, Filter.Tendsto, Filter.atTop, nhds, OfNat.ofNat, Filter.Eventually, SupSet.sSup, Set.ofPred, LE.le, HDiv.hDiv and 5 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   37 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_694 : ∀ᵉ (fmax : ℕ → ℕ) (fmin : ℕ → ℕ),
         (∀ n, (∃ m, Nat.totient m = n) → IsGreatest (Nat.totient ⁻¹' {n}) (fmax n)) →
         (∀ n, (∃ m, Nat.totient m = n) → IsLeast (Nat.totient ⁻¹' {n}) (fmin n)) →
         ∃ o : ℕ → ℝ, Tendsto o atTop (𝓝 0) ∧
           ∀ᶠ x : ℕ in atTop,
             sSup { (fmax n : ℝ) / fmin n | (n : ℕ) (_ : n ≤ x) (_ : ∃ m, Nat.totient m = n) } =
               (exp eulerMascheroniConstant + o x) * log (log (x : ℝ)) := by
   …

2. theorem Erdos694.erdos_694.variants.carmichael 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$ sorry line 68 source

   Source documentation

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

   depends on sorry what this means

   Statement uses: Iff, True, Exists, Nat, And, GT.gt, OfNat.ofNat, ExistsUnique, Eq, Nat.totient

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   4 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_694.variants.carmichael :
       answer(sorry) ↔ ∃ n > 0, ∃! m, Nat.totient m = n := by
   …

3. theorem Erdos694.erdos_694.variants.inf_unique 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$ sorry line 77 source

   Source documentation

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

   depends on sorry what this means

   Statement uses: Exists, Nat, And, GT.gt, OfNat.ofNat, ExistsUnique, Eq, Nat.totient, Set.Infinite, Set.ofPred

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   4 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

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