An infinite walk that never lines up three points
- What it is
- The paper claims an infinite three-dimensional grid walk with no three visited points in a line.
- Who did it
- Stijn Cambie and Erik Kalviainen
- What it could mean
- Walk forever on a three-dimensional grid without ever lining up three visited points. A verified construction would solve that astonishing puzzle using finite rules a computer can check.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
An infinite small-step (ℤ³)-walk with no collinear triple ↗See the proposed checks
In a separate ephemeral sandbox, inspect the pinned Lean theorem statements, imports, and axiom/trust-base report; map the sixteen-vector periodic or inductive construction in the manuscript to those statements; then independently check the finite no-three-collinear kernel and the inference to the infinite walk.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
- What it claims
- The manuscript claims an infinite walk in (ℤ³), using a fixed set of sixteen step vectors, whose vertices contain no collinear triple—answering the Gerver--Ramsey problem popularized as Erdős Problem 193. It is unusually ready for source-to-formal scope mapping because the arXiv record links both a Lean/formal project and a public project surface.
- Why this could matter
- An infinite walk that never lines up three points The construction solves a deceptively simple puzzle: move forever through a 3-D integer grid without ever placing three visited points on one line. It is also a compact test of machine-checked mathematics.
- If it holds up
- Foundational: it closes Erdős Problem 193 and supplies a reusable blueprint for formally verified infinite constructions built from finite, checkable rules.
- If it does not
- The puzzle remains open, while the mismatch would teach us where a finite checker or Lean statement failed to cover the infinite walk.
- Impact horizon
- Foundational · Discrete geometry · Formal verification · Combinatorics
- Version
- submitted 2026-09-01 18:37:21 UTC
- Why we tracked it
- a current claimed resolution of Erdős Problem 193 with a source-linked Lean 4 formalization, exact finite checks, and a separately inspectable public project; no docket created.
- Highest-risk dependency
- The core scope risk is whether the formal statement covers the whole infinite construction rather than only its finite kernel, and whether the manuscript's no-collinearity convention precisely matches the encoded predicate.
- Available artifacts
- The primary record explicitly links Lean 4 formalization, exact finite checks, and an interactive visualization. No artifact was run in this automation.
- Current boundary
- Intake record only; examination not started.