· via Hacker News – Front Page (native)
arXiv preprint claims Chair44, a decorated seven-cube solid, tiles 3D space only nonperiodically
A preprint by Ioannis Tsiokos presents Chair44, a seven-cube chair with pyramid features, claimed to be a single 3D tile whose every tiling is nonperiodic, with much of the proof machine-checked in Lean 4.

A strongly aperiodic monotile, in three dimensions
A preprint posted to arXiv claims to answer a question posed by Socolar and Taylor in tiling theory: does a single, simply connected three-dimensional prototile exist that forces nonperiodicity by shape alone? The paper, authored by Ioannis Tsiokos and submitted on 16 September 2026 as arXiv:2609.19214, presents a solid it calls Chair44 (R44) and argues that every tiling of space by congruent copies of it is nonperiodic. The work drew wider attention after reaching the Hacker News front page in mid-October 2026.
According to the abstract, earlier three-dimensional candidates fall short of the requirement. The Schmitt-Conway-Danzer biprism admits screw motions, and the three-dimensional Socolar-Taylor tile has a periodic stacking direction; both are therefore only weakly nonperiodic, leaving room for tilings that sidestep the intended aperiodic behaviour.
The tile itself
Chair44 is a rational polyhedral 3-ball: topologically a solid ball, assembled from seven unit cubes in a chair arrangement, with each of its 24 exposed unit-square panels carrying a small square-based pyramid. Those features act as a contact rule constraining how neighbouring copies may meet.
The claimed properties are strong. Per the abstract, the tile admits tilings of three-dimensional space by congruent copies, with reflections allowed. Yet every such tiling has no translational period, and the symmetry group of any tiling has order at most 24, meaning even the most symmetric tiling has only finite symmetry. Every tiling is homochiral, with all copies sharing one handedness even though mirrored copies are permitted, and every tiling carries a unique infinite hierarchy of nested supertiles, a self-similar structure in which each coarser level obeys the same rule.
How the proof works
The argument has two components. The first is a written geometric case that the pyramid features force any tiling onto a registered lattice. The second is a set of exhaustive finite enumerations, with the crux being a single finite test checked by machine: that the tile's contact rule survives coarsening, so the decoded parent tiling obeys the tile's rule and no other. That coarsening step is what propagates the argument up the hierarchy of supertiles.
The verification story is unusually thorough. The abstract reports that the companion census was replayed by two independent implementations, and that every finite gate was kernel-checked in Lean 4, modulo a named compiler hook for each native_decide theorem. The written geometric lemmas and the logical assembly were also formalised as Lean theorems, so the main result is kernel-checked subject to those named hooks, while the prose proofs are retained as exposition.
That modulo clause matters. Checks of the native_decide kind delegate work to compiled code rather than Lean's trusted kernel, so the guarantee rests on the named compiler hooks being sound. The abstract flags this openly rather than claiming unconditional kernel verification.
Caveats worth noting
This is a preprint, self-described as a proof submission, and it has not been peer reviewed. The abstract also attributes the tile's design to a reading of the aperiodic-monotile phenomenon via something called the Six Birds emergence calculus, covered in Section 3.3 of the paper and not explained in the abstract. Whether the finite enumerations and the Lean artefacts hold up under community scrutiny, including independent replay of the census and review of the compiler hooks, will determine whether the Socolar-Taylor question is genuinely settled.
Why it matters
If the claim survives review, it supplies the first strongly aperiodic monotile in three dimensions: one simply connected prototile whose every tiling is nonperiodic, with no weakly nonperiodic escape hatch such as a periodic stacking direction. That would close a question the field has circled since earlier 3D constructions showed aperiodicity was approachable but never forced. Beyond tiling theory, the paper is a case study in a proof pattern that is becoming standard in mathematics: a human geometric argument, exhaustive machine enumeration, and formal kernel checking stitched together, with the trust boundary of each component stated explicitly.
- #mathematics
- #formal-verification
- #lean
- #geometry
- #arxiv