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
Let be maximal such that if with then there is with such that if with then .
Estimate .
(fun n => ↑(Erdos789.subsetSumThreshold n)) =Θ[Filter.atTop] sorryOpenStatement only, no proof