Combinatorics

Erdős 340

Let

A = \{1, 2, 4, 8, 13, 21, 31, 45, 66, 81, 97, \ldots\}

be the greedy Sidon sequence: we begin with

1

and iteratively include the next smallest integer that preserves the Sidon property (i.e. there are no non-trivial solutions to

a + b = c + d

). What is the order of growth of

A

? Is it true that

|A \cap \{1, \ldots, N\}| \gg N^{1/2 - \varepsilon}

for all

\varepsilon > 0

and large

N

References

erdosproblems.com/340

No one has attempted this yet.

Formal statement

Lean type

∀ ε > 0, (fun n => √↑n / ↑n ^ ε) =O[Filter.atTop] fun n => ↑(Set.range Finset.greedySidon ∩ Set.Icc 1 n).ncard

What you must prove

import FormalConjectures.ErdosProblems.«340»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos340.erdos_340" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/340.lean

Source type SHA-256: sha256:d0bd6bbca81683d2f19d089c381cf1f17435eaeb8abaa9b27356681c76c08090
Task id: fc-379fc029-erdos340-erdos-340-e4f4c76d00-formalized-v1
Task commitment: sha256:3d37543fa1aa1bb45fd867e1c23f47fae844f3c23db2357254e9908f3f922ad0

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.