Skip to content

Erdős problem 1095

Start work

Erdős, Lacampagne, and Selfridge [ELS93] write 'it is clear to every right-thinking person' that g(k)≥exp⁡(cklog⁡k)g(k)\geq\exp(c\frac{k}{\log k}) for some constant c>0c>0.

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1095.lean

Retained formal statement2 of 4

Erdős, Lacampagne, and Selfridge [ELS93] write 'it is clear to every right-thinking person' that g(k)≥exp⁡(cklog⁡k)g(k)\geq\exp(c\frac{k}{\log k}) for some constant c>0c>0.

FormalConjectures/ErdosProblems/1095.leanErdos1095.erdos_1095.variants.lower_conjecture1 lineExact file
∃ c > 0, ∀ᶠ (k : ℕ) in Filter.atTop, ↑(Erdos1095.g k) ≥ Real.exp (c * ↑k / Real.log ↑k)
OpenStatement only, no proof