Skip to content

Erdős problem 156

Start work

Does there exist a maximal Sidon set A⊂{1,…,N}A\subset \{1,\ldots,N\} of size O(N1/3)O(N^{1/3})?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

156.lean

Retained formal statement1 of 4

Does there exist a maximal Sidon set A⊂{1,…,N}A\subset \{1,\ldots,N\} of size O(N1/3)O(N^{1/3})?

A question of Erdős, Sárközy, and Sós [ESS94].

FormalConjectures/ErdosProblems/156.leanErdos156.erdos_1561 lineExact file
True ↔ (fun N => ↑(Erdos156.minMaximalSidonSet N)) =O[Filter.atTop] fun N => ↑N ^ (1 / 3)
OpenStatement only, no proof