Erdős problem 390
Let be the least for which can be written as with - the smallest possible largest factor in a factorization of into distinct integers all exceeding . Erdős, Guy and Selfridge proved . Erdős asked whether there is a constant with and what it is.
Sources
FormalConjectures/ErdosProblems/
390.lean
Retained formal statement
f n - 2 * n = θ (n / log n). This is proved in [EGS82].
(fun n => ↑(Erdos390.f n) - 2 * ↑n) =Θ[Filter.atTop] fun n => ↑n / Real.log ↑nSolvedStatement only, no proof