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

FormalConjectures/ErdosProblems/

193.lean

Retained formal statement1 of 2

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?

FormalConjectures/ErdosProblems/193.leanErdos193.erdos_1936 linesExact file

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

OpenStatement only, no proof