How the Hilbert construction works
We want a robot to walk forever on the points of a 3D grid. It may use only a fixed collection of moves, and no three places it visits may ever lie on one straight line.
1. Begin with a path that fills a square
A Hilbert curve is a famous winding path. At each larger size, four smaller copies are turned and joined so the path visits every square in a grid without jumping.
Imagine those squares numbered in visiting order: 0, 1, 2, 3, and so on. Nearby numbers sit in touching squares.
2. Turn the flat path into a staircase
Now lift each square. Square 0 stays near the floor, square 1 goes to height 1, square 2 to height 2, and so on. The flat Hilbert path becomes a rising staircase in 3D.
The robot always rises, so it never returns to an old footprint.
3. The obvious staircase fails
If the robot lands on every stair, three consecutive landings can line up. The standard Hilbert path already fails at steps 3, 4, and 5.
Those three gold points lie on the red line in the diagram.
That quick failure was useful. It showed that the robot must skip some stairs—but not so many that it needs an unlimited collection of jumps.
4. Color squares by the way the path crosses them
Each small Hilbert piece has an entry and an exit. It can run right, up, down, or left. Those four directions are the four colors shown here.
A cell’s base-4 address tells the Hilbert rule which nested quarters to turn or flip. After the final turn, its entry-to-exit direction sets its color. The robot lands only on the blue, right-facing kind.
Another blue square always appears within 28 Hilbert places, so the robot never needs a giant leap.
5. Every connecting line gets a binary fingerprint
Pick any two chosen landings. Their Hilbert addresses reveal the first zoom level at which their floor positions separate. The proof turns that level into a number—a binary fingerprint for the connecting line.
If three landings formed one straight line, ordinary geometry and those fingerprints would demand two different scale changes at once. The red cross marks that impossible demand.
The argument works no matter how far the robot has walked, so it rules out every possible group of three.
6. The robot has a fixed menu of moves
Chosen landings are at most 28 Hilbert places apart, and consecutive Hilbert places touch on the floor. Every robot move therefore stays inside one fixed box.
The generated 500,000-step walk uses exactly the 16 arrows shown here. Their lengths range from 4.47 to 28.07 grid units.
7. Why the Lean proof matters
A program can test 500,000 steps, or a billion, but it still cannot test forever. Lean checks the chain from the Hilbert definitions to one theorem about every future step and every possible group of three.
The theorem has no unfinished proof holes and uses only standard Lean foundations. That turns a convincing pattern into a checkable infinite argument. Outside mathematicians still need to review that the formal statement exactly matches the original problem.
An unconditional infinite construction, checked by Lean; external mathematical review and community acceptance are pending.