Erdős problem 1095

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

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1095.lean

Retained formal statement3 of 4

The current record is $g(k) \gg \exp(c(\log k)^2)$ for some $c>0$ , due to Konyagin [Ko99b]. -

FormalConjectures/ErdosProblems/1095.leanErdos1095.erdos_1095.variants.lower_solved1 lineExact file

1∃ c > 0, (fun k => Real.exp (c * Real.log ↑k ^ 2)) =O[Filter.atTop] fun k => ↑(Erdos1095.g k)

SolvedStatement only, no proof