Erdős problem 789
Let be maximal such that if with then there is with such that if with then .
Sources
FormalConjectures/ErdosProblems/
789.lean
Retained formal statement
By the solved variant erdos_789.variants.isBigO_sq, in order to prove erdos_789.variants.sq it suffices to show .
(fun n => √↑n) =O[Filter.atTop] fun n => ↑(Erdos789.subsetSumThreshold n)OpenStatement only, no proof