Erdős problem 241
Is it true that ?
Sources
FormalConjectures/ErdosProblems/
241.lean
Retained formal statement
Is it true that ?
Originally asked to Erdős by Bose.
This is discussed in problem C11 of Guy's collection [Gu04].
True ↔ Asymptotics.IsEquivalent Filter.atTop (fun N => ↑(Erdos241.f N 3)) fun N => ↑N ^ (1 / 3)OpenStatement only, no proof