Erdős problem 539
For , how small can the cofactor set be? The answer is : a new upper bound matches the classical lower bound.
Sources
FormalConjectures/ErdosProblems/
539.lean
Retained formal statement
To prove erdos_539.variants.sq_cube_root it suffices to show .
(fun n => ↑n ^ (2 / 3)) =O[Filter.atTop] fun n => ↑(Erdos539.cofactorThreshold n)OpenStatement only, no proof