Compass-free Navigation of Mazes

If you find yourself in a corridor of a standard maze, a sure and easy way to escapeis to simply pick the left (or right) wall, and then follow it along its twists andturns and around the dead-ends till you eventually arrive at the exit. But whathappens when you cannot tell left from right? What if you cannot tell North fromSouth? What if you cannot judge distances, and have no idea what it means to followa wall in a given direction?The possibility of escape in these circumstances is suggested in the statement of anunproven theorem given in David Hilbert's celebrated /Foundations of Geometry/, inwhich he effectively claimed that a standard maze could be fully navigated usingaxioms and concepts based /solely/ on the relations of points lying on lines in aspecified order.We discuss our algorithm for this surprisingly challenging version of the mazenavigation problem, and our HOL Light verification of its correctness from Hilbert'saxioms.