Erdős problem 160
On Mathoverflow user leechlattice shows that .
Sources
FormalConjectures/ErdosProblems/
160.lean
Retained formal statement
Estimate by finding a better lower bound.
have lower_bound := sorry;(lower_bound =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)) ∧ ∀ c > 0, ((fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)) → ∀ c > 0, (fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =o[Filter.atTop] lower_boundOpenStatement only, no proof