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 statement4 of 4

Ecklund, Erdős, and Selfridge [EES74] conjectured g(k)≤exp⁡((1+o(1))k)g(k)\leq \exp((1+o(1))k).

FormalConjectures/ErdosProblems/1095.leanErdos1095.erdos_1095.variants.upper_conjecture1 lineExact file
∃ f, Filter.Tendsto f Filter.atTop (nhds 0) ∧ ∀ᶠ (k : ℕ) in Filter.atTop, ↑(Erdos1095.g k) ≤ Real.exp (↑k * (1 + f k))
OpenStatement only, no proof