Lift a Hilbert path into 3D
Use the Hilbert square number as height. This turns a flat, winding path into a staircase that always rises.
How the robot idea became a proof
The first Hilbert staircase did not work. Each failure narrowed the question until a small coloring rule and a binary fingerprint produced the final construction.
The robot cannot land on every stair
Steps 3, 4, and 5 already form a straight line. This exact counterexample killed the simplest version immediately.
Keeping corners or every few steps is not enough
Simple patterns still left straight-line triples. The landing rule had to use the way each small Hilbert piece is turned.
Four colors reveal a binary fingerprint
Squares with the same orientation color obey one exact rule connecting their floor separation to the difference between their path numbers.
Keep one color, with no long gaps
Two base-4 address digits are enough to guarantee another chosen square within 28 Hilbert places.
The fingerprint rules out every straight-line triple
A straight line would make the fingerprint scale in two incompatible ways. The contradiction works at every future distance.
500,000 steps reconstructed exactly
A separate program recomputed all 500,001 vertices and all 16 step choices from scratch. It matched the saved file exactly.
Every direction in the 500,000-step walk checked
A separate four-core verifier checked all 125,000,250,000 earlier-point directions. No direction repeated from any vertex, so no three recorded vertices are collinear.
The robot’s moves are proved to stay bounded forever
Lean proves the Hilbert path moves between neighbouring floor squares and that every chosen robot move belongs to one fixed finite set.
Unconditional AI-assisted proof; outside review pending
The complete Lean theorem constructs the infinite walk and rules out every group of three in a line. The next useful step is independent mathematical review.
Who did what
Erik Kalviainen, a math hobbyist and engineer, directed the research through prompts to GPT‑5.6 using Paseo and Oh My Pi as the working stack. Erik chose the questions, challenged conclusions, and steered the work toward exact checks and Lean. GPT‑5.6 performed much of the algebra, coding, testing, and formal proof development. The repository records both the successful route and the failed ideas.