These are the accompanying mathematical notes for the experimental research
project FRAP, Formalizing Rubik's
Abstract Polytopes. The project asks how the general mathematics of Rubik
puzzles can explain the concrete practice of solving them. Mathematical
exposition, formalization in Lean, and executable algorithms are intended to
develop together: understanding a puzzle should help us solve it, while
trying to solve it should sharpen the mathematics.
The motivation grew out of decades of playing the \(3\times 3\times 3\)
cube, followed by the \(2\times 2\times 2\) and \(4\times 4\times 4\). Learning
formulas raised questions about why they work, how different methods organize
a solve, and how a computer might find a better solution. Those questions led
back through group theory and the general \(N\times N\times N\) family to
Marchetti's Rubik's Abstract Polytopes [marchetti2025rubik].
These notes deliberately reverse that journey: begin with general mathematics,
develop increasingly concrete models, and return to solution methods and play
with a deeper understanding of the familiar puzzle.
A first concrete question guides the route: when a turn acts on one facet,
which positions move, and what incident labels travel with them? Starting with
abstract polytopes lets us answer that question in two stages. We first record
incidence and shape symmetry without choosing lengths or angles, then apply a
local facet action and inspect its effect on a tetrahedron and a cube. This
separation keeps the shape data distinct from the move data while giving each
abstraction a visible puzzle consequence. Passing to layered cubes then asks
how the pieces, their orientations and the allowed turns change with \(N\); the
\(3\times 3\times 3\) cube provides a setting in which to work out the consequences
in detail. Group actions connect these descriptions. They help us ask what a
move changes, what a sequence preserves, which configurations are reachable,
and how a solution can be assembled from smaller tasks. The additional
structure in each model must be explained when the models are compared.
The return to solving has two closely related purposes. For a person, a
useful formula connects a recognizable pattern with a manageable sequence of
moves. Understanding its effect and what it preserves should help explain
methods and the choices within a solve; recognition, memory and ease of
execution matter alongside move count. For a computer, the question is how to
find solutions under explicit objectives, including shortest solutions for a
chosen set of moves and costs. Producing a solution, proving that a method
solves every state in its domain, and establishing optimality are different
achievements. Scrambling, replay and interactive exploration bring these
questions back to actual use.
The puzzles also lead into mathematics beyond solving. Local orientation
data raise questions about global constraints, wreath products and transfer.
Transporting labels suggests comparisons with coloring obstructions and
branched coverings [izmestiev2002branched]. Random scrambles and functions
used to guide search lead to probability and representation theory
[pan2021fourier]. These are directions for inquiry,
with their own constructions and hypotheses; the aim is to understand the
connections through examples and arguments as well as the puzzles themselves.
Scholarly sources, explicit
calculations and formalization are meant to inform one another. Lean can
express mathematical models and implement computations whose stated properties
can be proved. Missing hypotheses or awkward conventions exposed by that work
should feed back into the explanations here. FRAP is at an early research
stage, and the companion repository does not yet contain a formalized puzzle
model or solver.