Erdős problem 1095
Erdős, Lacampagne, and Selfridge [ELS93] write 'it is clear to every right-thinking person' that for some constant .
Sources
FormalConjectures/ErdosProblems/
1095.lean
Retained formal statement
Erdős, Lacampagne, and Selfridge [ELS93] write 'it is clear to every right-thinking person' that for some constant .
∃ c > 0, ∀ᶠ (k : ℕ) in Filter.atTop, ↑(Erdos1095.g k) ≥ Real.exp (c * ↑k / Real.log ↑k)OpenStatement only, no proof