Skip to content

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

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

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

198.lean

Retained formal statement3 of 4

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 P1,P2,P_1,P_2,\ldots be an enumeration of all countably many infinite arithmetic progressions. We choose a1a_1 to be the minimal element of P1NP_1\cap \mathbb{N}, and in general choose ana_n to be an element of PnNP_n\cap \mathbb{N} such that an>2an1a_n>2a_{n-1}. By construction A={a1<a2<}A=\{a_1 < a_2 < \cdots\} 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: A={(n+1)!+n:n0}A = \{ (n+1)!+n : n\geq 0\}. This is a Sidon set, and intersects every arithmetic progression, since for any a,dNa,d\in \mathbb{N}, (a+d+1)!+(a+d)A(a+d+1)!+(a+d)\in A, and dd divides (a+d+1)!+d(a+d+1)!+d.

This was formalized in Lean by Alexeev using Aristotle.

FormalConjectures/ErdosProblems/198.leanErdos198.erdos_1981 lineExact file
(∀ (A : Set ℕ), IsSidon A → ∃ Y, Y.IsAPOfLength ⊤ ∧ YAᶜ) ↔ False
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