Erdős problem 314
Let and let be minimal such that . We define How small can be? Is it true that
Sources
FormalConjectures/ErdosProblems/
314.lean
Retained formal statement
Let and let be minimal such that . We define How small can be? Is it true that
This is true, and shown by Lim and Steinerberger [LiSt24], who further proved that, for any , there exist infinitely many and such that Erdős and Graham (and also Lim and Steinerberger) believe that the exponent of is best possible here, in that for all .
True ↔ Filter.liminf (fun n => ↑n ^ 2 * Erdos314.epsilon n) Filter.atTop = 0