Combinatorics · Last catalog review 26 Jul 2026

Erdős Problem 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

Published 18 Jul 2026Never attempted

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-e923379e-erdos340-erdos-340-a94c373747-formalized-v1
Task commitment: sha256:7ce02b4c75d6dbe537eb99d36614a7adda2a4b145d9df49cff310e2e17478f76

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.