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 .
Is ?
(fun n => ↑(Erdos789.subsetSumThreshold n)) =Θ[Filter.atTop] fun n => (↑n * Real.log ↑n) ^ (1 / 3)OpenStatement only, no proof