Erdős problem 933
If , where , then is it true that ?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/933.leanTrue ↔ Filter.limsup (fun n => ↑↑(2 ^ Erdos933.k n * 3 ^ Erdos933.l n) / (↑↑n * ↑(Real.log ↑n))) Filter.atTop = ⊤OpenStatement only, no proof