An infinite small-step ${\mathbb{Z}}^3$-walk with no collinear triple

Abstract

We construct an infinite walk in ${\mathbb{Z}}^3$ whose steps come from a fixed set of sixteen vectors and no three of whose vertices are collinear, answering a problem of Gerver and Ramsey popularized as Erdős Problem 193.

2 pages. Lean 4 formalization, exact finite checks, and interactive visualization are available at https://erdos-193.q5m.ai and https://github.com/ekalvi/erdos-193