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
Straus [Str66] proved that .
(fun n => ↑(Erdos789.subsetSumThreshold n)) =O[Filter.atTop] fun n => √↑nSolvedStatement only, no proof