AI 中文总结
本文构造了$\text{Z}^3}$中步长取自16个固定向量的无限游走，无三个顶点共线，解决了由Erdős问题193推广的Gerver与Ramsey问题。
AI 中文摘要
我们在$\text{Z}^3}$中构造了一种无限游走，其步长来自固定的16个向量集合，且顶点中无三个共线，解决了由Erdős问题193推广的Gerver与Ramsey问题。
英文摘要
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.
Comments2 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
