Erdős problem 198
The answer is no; Erdős and Graham report this was proved by Baumgartner, presumably referring to the paper [Ba75], which does not state this exactly, but the following simple construction is implicit in [Ba75].
Sources
FormalConjectures/ErdosProblems/
198.lean
The answer is no; Erdős and Graham report this was proved by Baumgartner, presumably referring to the paper [Ba75], which does not state this exactly, but the following simple construction is implicit in [Ba75].
Let be an enumeration of all countably many infinite arithmetic progressions. We choose to be the minimal element of , and in general choose to be an element of such that . By construction contains at least one element from every infinite arithmetic progression, and is a lacunary set, so is certainly Sidon.
AlphaProof has found the following explicit construction: . This is a Sidon set, and intersects every arithmetic progression, since for any , , and divides .
This was formalized in Lean by Alexeev using Aristotle.
(∀ (A : Set ℕ), IsSidon A → ∃ Y, Y.IsAPOfLength ⊤ ∧ Y ⊆ Aᶜ) ↔ False