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
Erdős [Er62c] and Choi [Ch74b] proved that .
(fun n => (↑n * Real.log ↑n) ^ (1 / 3)) =O[Filter.atTop] fun n => ↑(Erdos789.subsetSumThreshold n)SolvedStatement only, no proof