Erdős Problem #193
DISPROVED LEANdatabase updated 2026-09-04
The statement as posed is false. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
An \(S\)-walk is a sequence where every difference is in \(S\).
True if set \(A\) contains 3 distinct collinear points over \(R\).
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? Cambie and Kalviainen [CaKa26] answered this question in the negative by constructing an infinite walk in \(\mathbb{Z}^3\) with a finite set of steps and no three collinear points.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/193.Prizenone
Topicsgeometry
Statement in LeanFormal Conjectures
Solution in Leanyes
OEISA231255
Original pageerdosproblems.com/193
Attempts
submit one →Read our working report →
Live page status OPEN; “Currently working on this problem” lists ekalvi (checked 2026-07-28), so the mandatory no-collision rule forbids an attempt.
SKIPPED