A robot can walk forever on a 3D grid without any three footprints lining up.
That gives a negative answer to Erdős Problem 193, which asks whether every such walk must contain three collinear points. This repository contains a complete construction and a computer-checked proof. Outside mathematical review is still pending.
Make a staircase from a Hilbert fractal, then let the robot land only on specially marked steps.
The four ideas below are enough to understand the shape of the solution. The detailed proof explains why they work for every future step.
A Hilbert curve is a single winding route that visits every square in a square grid.
Give each visited square a height equal to its place in the route. The flat path becomes a rising 3D staircase.
Each square has one of four simple “states.” The robot lands only on one state, never skipping too far.
Every line between two chosen steps carries a number that prevents three chosen steps from lining up.
It never needs a giant jump.
The robot may skip some Hilbert squares, but it always reaches another chosen square within 28 places. Neighbouring Hilbert squares touch, so a short skip in the route is also a bounded move across the floor.
That gives one fixed, finite menu of 3D moves. The 500,000-step example uses exactly 16 different moves.
See the walk and all 16 moves →Every connecting line has a binary fingerprint.
The Hilbert address of two chosen steps tells us exactly how many times their separation can be divided by two. Three points on one straight line would force the same fingerprint to change in two incompatible ways.
That contradiction applies to any three steps, no matter how far into the future they occur.
Follow the plain-language proof →A 500,000-step check cannot prove “forever.” Lean can check the general argument.
Lean is a proof-checking system. The proof is written as small logical steps, and Lean’s compact trusted core checks that every step follows from the definitions and earlier results. It checks the rule for all natural-number positions—not only the large example we generated.
The Lean project builds successfully without unfinished placeholders or project-specific assumptions. That is strong evidence that the logical chain is complete. It does not replace outside mathematical review of whether the definitions exactly match Erdős Problem 193.
Human-steered, AI-assisted mathematics
Erik Kalviainen, a math hobbyist and engineer in Canada, used Paseo, Oh My Pi, and GPT‑5.6 as the working stack for an AI research partner. Erik steered the work through prompts: proposing the robot idea, choosing which failures to investigate, demanding exact counterexamples, and directing the move into Lean.
GPT‑5.6 translated those prompts into algebra, searches, adversarial tests, code, and formal proofs. The first obvious Hilbert staircase failed almost immediately; the human-and-AI loop used that failure to discover the state selector and binary fingerprint that make the final construction work.
The repository keeps the generated artifacts, independent verifier, Lean source, and failed routes visible so the claim can be checked rather than taken on trust.
Explore the construction
Orbit the exact 500,000-step path, pause it, adjust its displayed height, and inspect every allowed move.
Hilbert state mapSee why the robot visits only one kind of square and why those squares are never too far apart.
Proof status and Lean checksThe exact theorem, what Lean checked, what computation checked, and what still needs outside review.