Erdős problem 193

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?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

193.lean

Retained formal statement2 of 2

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

FormalConjectures/ErdosProblems/193.leanErdos193.erdos_193_z24 linesExact file

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

SolvedStatement only, no proof