What Lean checked
The repository contains a complete counterexample construction for Erdős Problem 193, giving a negative answer to its “must every walk?” question. Lean checked the infinite construction—not only the 500,000-step example. External mathematical review is still pending.
Ordinary testing can only check a finite number of robot steps. Lean checks the general argument for every future step and every possible group of three footprints. Its small trusted core rejects a proof if even one required logical step is missing.
Exact theorem shape
S.Finite ∧
(∀ n, displacement (P n) (P (n+1)) ∈ S) ∧
(∀ i<j<k, ¬ OrderedCollinear (P i) (P j) (P k))
Point3 has three integer coordinates. Because the third coordinate of P is strictly increasing, the ordered formulation covers every triple of distinct vertices after sorting by index.
Dependency chain
Transducer.lean defines base-4 digits, square orientations, emitted coordinate bits, forward states, and exact inverse transitions.
Valuation.lean defines the planar pair valuation and proves its integer-scaling law.
PairLaw.lean proves the equal- and unequal-length terminal-state pair identities for arbitrary words.
Construction.lean defines even padding, terminal steering, bounded index gaps, the selected lift, and the collinearity contradiction.
Continuity.lean proves discrete Hilbert adjacency, coordinate-model equivalence, the universal planar bound, and finite-step membership.
The fixed step set
The theorem uses the explicit finite superset
The proof does not assume that this is the smallest menu. It is a simple finite box containing every consecutive displacement. The generated 500,000-step prefix realizes exactly 16 distinct vectors.
Axiom audit
[propext, Classical.choice, Quot.sound]
These are standard foundations used by Lean and Mathlib. The theorem uses no repository-specific axiom, no sorry, and no native_decide trust shortcut.
Independent finite checks
hilbert-193-500k.jsonl contains 500,001 exact integer vertices with digest 6f8fdf59…143d63.
One verifier rebuilds the selector, coordinates, steps, and all 16 realized vectors without importing the constructor.
A second verifier checks every primitive direction from every vertex to its predecessors. None repeats, so no three recorded vertices are collinear.
These finite checks validate the recorded example and independent implementations. They are not used to discharge any all-index proposition in Lean.
Review boundary
A machine-checked proof can still formalize the wrong statement. The remaining human review questions are therefore concrete:
- Does
OrderedCollinear, together with strictly increasing height, match ordinary collinearity for every triple of distinct vertices? - Does the nested-even transducer equal the intended standard discrete Hilbert indexing?
- Does the finite-menu theorem exactly match the fixed-finite-step requirement in the Gerver–Ramsey problem?
- Are the source definitions free of an accidental narrowed domain?
The construction gives a negative answer to the original question, supported by the formal bridge lemmas and independent replay. External mathematical review is still pending.