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
Let be maximal such that, for any set of size , the sethas size at least . Estimate .
(fun n => ↑(Erdos539.cofactorThreshold n)) =Θ[Filter.atTop] sorryOpenStatement only, no proof