Erdős Problem 193

References:

• erdosproblems.com/193
• [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
• [GeRa79] Gerver, Joseph L. and Ramsey, L. Thomas, "On certain sequences of lattice points." Pacific J. Math. (1979), 357-363.

def Erdos193.IsSWalk {V : Type u_1} [AddCommGroup V] (S : Set V) (a : ℕ → V) : Prop

An $S$-walk is a sequence where every difference is in $S$.

Equations

• Erdos193.IsSWalk S a = ∀ (n : ℕ), a (n + 1) - a n ∈ S

def Erdos193.HasCollinearTriple (R : Type u_2) {V : Type u_1} [DivisionRing R] [AddCommGroup V] [Module R V] (A : Set V) : Prop

True if set $A$ contains 3 distinct collinear points over $R$.

Equations

• Erdos193.HasCollinearTriple R A = ∃ x ∈ A, ∃ y ∈ A, ∃ z ∈ A, x ≠ y ∧ y ≠ z ∧ x ≠ z ∧ Collinear R {x, y, z}

theorem Erdos193.erdos_193 : True ↔ ∀ (S : Set (Fin 3 → ℤ)), S.Finite → ∀ (a : ℕ → Fin 3 → ℤ), IsSWalk S a → (Set.range a).Infinite → HasCollinearTriple ℚ (Set.range fun (n : ℕ) => Int.cast ∘ a n)

Let $S \subseteq \mathbb{Z}^3$ be a finite set and let $A = \lbrace a_1, a_2, \ldots \rbrace$ be an infinite $S$-walk, so that $a_{i+1} - a_i \in S$ for all $i$. Must $A$ contain three collinear points?

theorem Erdos193.erdos_193_z2 (S : Set (Fin 2 → ℤ)) : S.Finite → ∀ (a : ℕ → Fin 2 → ℤ), IsSWalk S a → (Set.range a).Infinite → HasCollinearTriple ℚ (Set.range fun (n : ℕ) => Int.cast ∘ a n)

[GeRa79] showed that the answer is yes for $\mathbb{Z}^2$