Erdős problem 193
Let be a finite set and let be an infinite -walk, so that for all . Must contain three collinear points?
Sources
FormalConjectures/ErdosProblems/
193.lean
Retained formal statement
[GeRa79] showed that the answer is yes for
∀ (S : Set (Fin 2 → ℤ)), S.Finite → ∀ (a : ℕ → Fin 2 → ℤ), Erdos193.IsSWalk S a → (Set.range a).Infinite → Erdos193.HasCollinearTriple ℚ (Set.range fun n => Int.cast ∘ a n)SolvedStatement only, no proof