Erdős problem 933
If , where , then is it true that ?
Sources
FormalConjectures/ErdosProblems/
933.lean
Retained formal statement
Mahler proved (a more general result that implies in particular) that .
∃ c, c =o[Filter.atTop] 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(2 ^ Erdos933.k n * 3 ^ Erdos933.l n) < ↑n ^ (1 + c n)SolvedStatement only, no proof