Summary
An arXiv preprint describes Chair44, a single polyhedral tile that the author says fills three-dimensional space only in arrangements with no translational period. The reported proof combines geometric constraints with exhaustive finite checks and Lean 4 formalization.
An arXiv preprint by Ioannis Tsiokos describes Chair44 (R44), a single three-dimensional shape that tiles space while forcing every tiling to lack a translational period. The paper, submitted on 16 September 2026, presents the result as a proof of a strongly aperiodic monotile: one shape that can fill space, but cannot form a pattern that repeats unchanged after a translation.
The result concerns the geometry of the tile itself, rather than a set of differently coloured pieces or extra labels. The paper says Chair44 is a rational polyhedral 3-ball: a solid with flat faces and no holes, with vertices at rational coordinates. Its shape resembles a chair assembled from seven cubes; 24 exposed unit-square panels carry small square-pyramid features.
How the shape constrains a tiling
The author says the pyramid features force every possible tiling onto a registered lattice. In a tiling, copies of a shape meet along their boundaries; here, the features restrict which contacts can fit. The paper’s geometric argument uses those restrictions to establish the lattice structure, while finite enumerations check which arrangements are possible.
The result applies to tilings made from congruent copies, with reflections allowed. Even so, the abstract reports that every tiling is homochiral—its tiles all have the same handedness—and has a unique infinite hierarchy of nested “supertiles”. These are larger-scale groupings of tiles that can themselves be treated as units. The abstract also says that each tiling’s symmetry group has order at most 24. This allows for some finite symmetries, while ruling out a translational period.
A proof combining geometry and computation
The proof description combines written geometric arguments with exhaustive finite checks. A central test checks that the tile’s contact rule survives coarsening: when a tiling is decoded into larger parent units, the resulting arrangement still follows that contact rule and no additional one. The abstract says this gives the nested hierarchy while preserving the constraints needed for aperiodicity.
The author reports that two independent implementations replay the finite census. The finite gates, geometric lemmas and logical assembly are also formalized in Lean 4. The abstract qualifies its kernel-checking claim: each native_decide theorem uses a named compiler hook. This qualification is part of the paper’s description of how the proof was checked.
The mathematical significance is the reported construction of one simply connected three-dimensional tile whose geometry alone forces non-periodic tilings. The result is presented in an arXiv preprint, rather than as a claim about a physical material or a manufactured object.