Erdős problem 862
Let be the number of maximal Sidon subsets of . Is it true that for some constant ?
Sources
FormalConjectures/ErdosProblems/
862.lean
Retained formal statement
Let be the number of maximal Sidon subsets of . Is it true that
A problem of Cameron and Erdős. This is resolved as a consequence of results of Saxton and Thomason [SaTh15] - they prove that the number of Sidon sets in is at least . Since each Sidon set is contained in a maximal Sidon set, and each maximal Sidon set contains at most Sidon sets, it follows that
False ↔ (fun N => Real.logb 2 ↑(Erdos862.numMaximalSidonSets N)) =o[Filter.atTop] fun N => ↑N ^ (1 / 2)