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
Does there exists a constant c such that f n - 2 * n ~ c * (n / log n)?
True ↔ ∃ c, Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos390.f n) - 2 * ↑n) fun n => c * ↑n / Real.log ↑nOpenStatement only, no proof