Erdős problem 304
Is it true that ?
Sources
FormalConjectures/ErdosProblems/
304.lean
Retained formal statement
In 1950, Erdős [Er50c] proved the upper bound . [Er50c] Erdős, P., Az egyenlet egÉsz szÁmú megoldÁsairól. Mat. Lapok (1950), 192-210.
(fun b => ↑(Erdos304.smallestCollectionTo b)) =O[Filter.atTop] fun b => Real.log ↑b / Real.log (Real.log ↑b)SolvedStatement only, no proof