Erdős Problem 198

References:

• erdosproblems.com/198
• [Ba75] Baumgartner, James E., Partitioning vector spaces. J. Combinatorial Theory Ser. A (1975), 231-233.

theorem Erdos198.baumgartner_strong (V : Type u_1) [AddCommGroup V] [Module ℚ V] (k : ℕ) : ∃ (X : Set V), (∀ (Y : Set V), Y.IsAPOfLength ⊤ → (X ∩ Y).Nonempty) ∧ ∀ (Y : Set V), Y.IsAPOfLength ↑k → (X ∩ Y).ncard ≤ 2

Let $V$ be a vector space over the rationals and let $k$ be a fixed positive integer. Then there is a set $X_k \subseteq V$ such that $X_k$ meets every infinite arithmetic progression in $V$ but $X_k$ intersects every $k$-element arithmetic progression in at most two points.

At the end of [Ba75] the author claims that by "slightly modifying the method of [his proof]", one can prove this.

theorem Erdos198.baumgartner_headline (V : Type u_1) [AddCommGroup V] [Module ℚ V] : ∃ (X : Set V), (∀ (Y : Set V), Y.IsAPOfLength ⊤ → (X ∩ Y).Nonempty) ∧ ∀ (Y : Set V), Y.IsAPOfLength 3 → (X ∩ Y).ncard ≤ 2

The statement for which Baumgartner actually writes a proof.

theorem Erdos198.erdos_198 : (∀ (A : Set ℕ), IsSidon A → ∃ (Y : Set ℕ), Y.IsAPOfLength ⊤ ∧ Y ⊆ Aᶜ) ↔ False

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 $P_1,P_2,\ldots$ be an enumeration of all countably many infinite arithmetic progressions. We choose $a_1$ to be the minimal element of $P_1\cap \mathbb{N}$, and in general choose $a_n$ to be an element of $P_n\cap \mathbb{N}$ such that $a_n>2a_{n-1}$. By construction $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 : n\geq 0\}$. This is a Sidon set, and intersects every arithmetic progression, since for any $a,d\in \mathbb{N}$, $(a+d+1)!+(a+d)\in A$, and $d$ divides $(a+d+1)!+d$.

This was formalized in Lean by Alexeev using Aristotle.

theorem Erdos198.erdos_198.variants.concrete : ∃ (A : Set ℕ), A = {x : ℕ | ∃ (n : ℕ), n.factorial + n = x} ∧ IsSidon A ∧ ∀ (Y : Set ℕ), Y.IsAPOfLength ⊤ → (A ∩ Y).Nonempty

In fact one such sequence is $n! + n$. This was found by AlphaProof. It also found $(n + 1)! + n$.