Skip to content

Erdős problem 862

Let A1(N)A_1(N) be the number of maximal Sidon subsets of {1,,N}\{1,\ldots,N\}. Is it true that A1(N)>2NcA_1(N) > 2^{N^c} for some constant c>0c>0?

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

862.lean

Retained formal statement1 of 3

Let A1(N)A_1(N) be the number of maximal Sidon subsets of {1,,N}\{1,\ldots,N\}. Is it true that A1(N)<2o(N1/2)?A_1(N) < 2^{o(N^{1/2})}?

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 {1,,N}\{1,\ldots,N\} is at least 2(1.16+o(1))N1/22^{(1.16+o(1))N^{1/2}}. Since each Sidon set is contained in a maximal Sidon set, and each maximal Sidon set contains at most 2(1+o(1))N1/22^{(1+o(1))N^{1/2}} Sidon sets, it follows that A1(N)2(0.16+o(1))N1/2.A_1(N) \geq 2^{(0.16+o(1))N^{1/2}}.

FormalConjectures/ErdosProblems/862.leanErdos862.erdos_862.parts.i1 lineExact file
False ↔ (fun N => Real.logb 2 ↑(Erdos862.numMaximalSidonSets N)) =o[Filter.atTop] fun N => ↑N ^ (1 / 2)
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Search problems.science

Find a Problem, Result, source, or page