Erdős problem 39 · problems.science

Is there an infinite Sidon set $A\subset \mathbb{N}$ such that $\lvert A\cap \{1\ldots,N\}\rvert \gg_\epsilon N^{1/2-\epsilon}$ for all $\varepsilon > 0$ ?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

39.lean

Retained formal statement1 of 1

Is there an infinite Sidon set $A\subset \mathbb{N}$ such that $\lvert A\cap \{1\ldots,N\}\rvert \gg_\epsilon N^{1/2-\epsilon}$ for all $\varepsilon > 0$ ?

FormalConjectures/ErdosProblems/39.leanErdos39.erdos_392 linesExact file

1True ↔2  ∃ A, A.Infinite ∧ IsSidon A ∧ ∀ ε > 0, (fun x => ↑x ^ (1 / 2 - ε)) =O[Filter.atTop] fun N => ↑(Set.Icc 1 N ∩ A).ncard

OpenStatement only, no proof

Sources

Search problems.science