Erdős problem 156
Does there exist a maximal Sidon set of size ?
Sources
FormalConjectures/ErdosProblems/
156.lean
Retained formal statement
Does there exist a maximal Sidon set of size ?
A question of Erdős, Sárközy, and Sós [ESS94].
True ↔ (fun N => ↑(Erdos156.minMaximalSidonSet N)) =O[Filter.atTop] fun N => ↑N ^ (1 / 3)OpenStatement only, no proof