FormalConjectures.ErdosProblems.«933»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Erdős Problem 933

References:

erdosproblems.com/933

[Er76d] Erdős, P, Problems and results on number theoretic properties of consecutive integers and related questions. Proceedings of the Fifth Manitoba Conference on Numerical Mathematics (Univ. Manitoba, Winnipeg, Man., 1975) (1976), 25-44.

open Filternamespace Erdos933

The 2-adic valuation of $n(n+1)$.

def k (n : ℕ) : ℕ := padicValNat 2 (n * (n + 1))

The 3-adic valuation of $n(n+1)$.

def l (n : ℕ) : ℕ := padicValNat 3 (n * (n + 1))

If $n(n+1)=2^k3^lm$, where $(m,6)=1$, then is it true that $\limsup_{n\to \infty} \frac{2^k3^l}{n\log n}=\infty$?

@[category research open, AMS 11]
theorem erdos_933 :
    answer(sorry) ↔
      atTop.limsup (fun n : ℕ ↦
        ((((2 ^ k n * 3 ^ l n : ℕ) : ℝ) / ((n : ℝ) * Real.log (n : ℝ))) : EReal)) = ⊤ := by⊢ True ↔ limsup (fun n ↦ ↑↑(2 ^ k n * 3 ^ l n) / (↑↑n * ↑(Real.log ↑n))) atTop = ⊤
  sorryAll goals completed! 🐙

Mahler proved (a more general result that implies in particular) that $2^k3^l<n^{1+o(1)}$.

@[category research solved, AMS 11]
theorem erdos_933.variants.mahler :
    ∃ c : ℕ → ℝ, (c =o[atTop] (1 : ℕ → ℝ)) ∧
      ∀ᶠ n in atTop, ((2 ^ k n * 3 ^ l n : ℕ) : ℝ) < (n : ℝ) ^ (1 + c n) := by⊢ ∃ c, c =o[atTop] 1 ∧ ∀ᶠ (n : ℕ) in atTop, ↑(2 ^ k n * 3 ^ l n) < ↑n ^ (1 + c n)
  sorryAll goals completed! 🐙

Erdős [Er76d] wrote 'it is easy to see' that for infinitely many $n$, $2^k 3^l > n\log n$.

Steinerberger has noted a simple proof of this fact follows from taking $n=2^{3^r}$ for any integer $r\geq 1$, when $k=3^r$ and $l=r+1$.


@[category research solved, AMS 11]
theorem erdos_933.variants.lower_bound :
    Set.Infinite { n : ℕ | ((2 ^ k n * 3 ^ l n : ℕ) : ℝ) > (n : ℝ) * Real.log (n : ℝ) } := by⊢ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}.Infinite
  -- Witness: n = 2^(3^(r+1)); k n = 3^(r+1), l n = r+2 by LTE, and 3 > log 2.
  refine Set.infinite_of_injective_forall_mem
    (f := fun r : ℕ ↦ 2 ^ (3 ^ (r + 1))) ?_ fun r ↦ ?_refine_1⊢ Function.Injective fun r ↦ 2 ^ 3 ^ (r + 1)refine_2r:ℕ⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}
  ·refine_1⊢ Function.Injective fun r ↦ 2 ^ 3 ^ (r + 1) exact (Nat.pow_right_injective (a := 2) (by⊢ 2 ≤ 2 norm_numAll goals completed! 🐙)).comp
      ((Nat.pow_right_injective (a := 3) (by⊢ 2 ≤ 3 norm_numAll goals completed! 🐙)).comp (add_left_injective 1))
  let m := 3 ^ (r + 1)refine_2r:ℕm:ℕ := 3 ^ (r + 1)⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}
  have hk : k (2 ^ m) = m := by⊢ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}.Infiniterefine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}
    rw [k,r:ℕm:ℕ := 3 ^ (r + 1)⊢ padicValNat 2 (2 ^ m * (2 ^ m + 1)) = mrefine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} padicValNat.mul (byr:ℕm:ℕ := 3 ^ (r + 1)⊢ 2 ^ m ≠ 0refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} positivityAll goals completed! 🐙refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}) (byr:ℕm:ℕ := 3 ^ (r + 1)⊢ 2 ^ m + 1 ≠ 0refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} positivityAll goals completed! 🐙refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}), padicValNat.prime_pow,r:ℕm:ℕ := 3 ^ (r + 1)⊢ m + padicValNat 2 (2 ^ m + 1) = mrefine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}
      padicValNat.eq_zero_of_not_dvd
        ((Even.pow_of_ne_zero (byr:ℕm:ℕ := 3 ^ (r + 1)⊢ Even 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} norm_numAll goals completed! 🐙refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}) (byr:ℕm:ℕ := 3 ^ (r + 1)⊢ m ≠ 0refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} positivityAll goals completed! 🐙refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n})).add_one).not_two_dvd_nat, add_zeror:ℕm:ℕ := 3 ^ (r + 1)⊢ m = mrefine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}]refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}
  have hl : l (2 ^ m) = r + 2 := by⊢ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}.Infiniterefine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}
    rw [l,r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 ^ m * (2 ^ m + 1)) = r + 2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 ^ m + 1) = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} padicValNat.mul (byr:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 2 ^ m ≠ 0r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 ^ m + 1) = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} positivityAll goals completed! 🐙r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 ^ m + 1) = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}) (byr:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 2 ^ m + 1 ≠ 0r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 ^ m + 1) = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} positivityAll goals completed! 🐙r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 ^ m + 1) = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}),
      padicValNat_prime_prime_pow (p := 3) (q := 2) m (byr:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 3 ≠ 2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 ^ m + 1) = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} norm_numAll goals completed! 🐙r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 ^ m + 1) = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}), zero_addr:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 ^ m + 1) = r + 2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 ^ m + 1) = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}]r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 ^ m + 1) = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}
    rw [show 2 ^ m + 1 = 2 ^ m + 1 ^ m by⊢ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}.Infiniter:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 + 1) + padicValNat 3 m = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} simpAll goals completed! 🐙r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 + 1) + padicValNat 3 m = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n},
      padicValNat.pow_add_pow (p := 3) (x := 2) (y := 1) (byr:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ Odd 3r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 + 1) + padicValNat 3 m = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} norm_numAll goals completed! 🐙r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 + 1) + padicValNat 3 m = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n})
        (byr:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 3 ∣ 2 + 1r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 + 1) + padicValNat 3 m = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} norm_numAll goals completed! 🐙r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 + 1) + padicValNat 3 m = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}) (byr:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ ¬3 ∣ 2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 + 1) + padicValNat 3 m = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} norm_numAll goals completed! 🐙r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 + 1) + padicValNat 3 m = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}) (byr:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ Odd mr:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 + 1) + padicValNat 3 m = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} simpa [m] using (byr:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ Odd 3r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 + 1) + padicValNat 3 m = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} norm_numAll goals completed! 🐙r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 + 1) + padicValNat 3 m = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} : Odd 3).pow)]r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ padicValNat 3 (2 + 1) + padicValNat 3 m = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}
    simp [m]r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m⊢ 1 + (r + 1) = r + 2refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}
    liarefine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}
  have hlog : (m : ℝ) * Real.log 2 < (3 : ℝ) ^ (r + 2) := by⊢ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}.Infiniterefine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2hlog:↑m * Real.log 2 < 3 ^ (r + 2)⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}
    calc
      _ < (m : ℝ) * 3 := mul_lt_mul_of_pos_left (byr:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ Real.log 2 < 3refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2hlog:↑m * Real.log 2 < 3 ^ (r + 2)⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} linarith [Real.log_two_lt_d9]All goals completed! 🐙refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2hlog:↑m * Real.log 2 < 3 ^ (r + 2)⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}) (byr:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ 0 < ↑mrefine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2hlog:↑m * Real.log 2 < 3 ^ (r + 2)⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} positivityAll goals completed! 🐙refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2hlog:↑m * Real.log 2 < 3 ^ (r + 2)⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n})
      _ = _ := byr:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2⊢ ↑m * 3 = 3 ^ (r + 2)refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2hlog:↑m * Real.log 2 < 3 ^ (r + 2)⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n} norm_num [m, pow_succ]refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2hlog:↑m * Real.log 2 < 3 ^ (r + 2)⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2hlog:↑m * Real.log 2 < 3 ^ (r + 2)⊢ 2 ^ 3 ^ (r + 1) ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}
  change 2 ^ m ∈ {n | ((2 ^ k n * 3 ^ l n : ℕ) : ℝ) > (n : ℝ) * Real.log (n : ℝ)}refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2hlog:↑m * Real.log 2 < 3 ^ (r + 2)⊢ 2 ^ m ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}
  simp only [Set.mem_ofPred_eq, hk, hl]refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2hlog:↑m * Real.log 2 < 3 ^ (r + 2)⊢ ↑(2 ^ m * 3 ^ (r + 2)) > ↑(2 ^ m) * Real.log ↑(2 ^ m)
  push_castrefine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2hlog:↑m * Real.log 2 < 3 ^ (r + 2)⊢ 2 ^ m * 3 ^ (r + 2) > 2 ^ m * Real.log (2 ^ m)
  rw [Real.log_powrefine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2hlog:↑m * Real.log 2 < 3 ^ (r + 2)⊢ 2 ^ m * 3 ^ (r + 2) > 2 ^ m * (↑m * Real.log 2)refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2hlog:↑m * Real.log 2 < 3 ^ (r + 2)⊢ 2 ^ m * 3 ^ (r + 2) > 2 ^ m * (↑m * Real.log 2)]refine_2r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2hlog:↑m * Real.log 2 < 3 ^ (r + 2)⊢ 2 ^ m * 3 ^ (r + 2) > 2 ^ m * (↑m * Real.log 2)
  exact mul_lt_mul_of_pos_left hlog (byr:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = mhl:l (2 ^ m) = r + 2hlog:↑m * Real.log 2 < 3 ^ (r + 2)⊢ 0 < 2 ^ m positivityAll goals completed! 🐙)

end Erdos933