+- MKLab (https://mklab.gr)
+-- Forum: [INDEX] (https://mklab.gr/forumdisplay.php?fid=1)
+--- Forum: MATHEMATICS (https://mklab.gr/forumdisplay.php?fid=3)
+---- Forum: ARTICLES (https://mklab.gr/forumdisplay.php?fid=13)
+----- Forum: GEOMETRY (https://mklab.gr/forumdisplay.php?fid=150)
+----- Thread: Software developer finds first 3D “einstein” tile (/showthread.php?tid=2168)
Software developer finds first 3D “einstein” tile - mklabgr - 09-25-2026
The paper “A Strongly Aperiodic Monotile in Three Dimensions” by Ioannis Tsiokos, submitted to arXiv in September 2026, presents a remarkable solution to a long-standing tiling problem in three-dimensional space. The author constructs a single three-dimensional shape, called Chair44 or $Q$, that can tile all of $\mathbb{R}^3$ using congruent copies, but cannot produce any tiling with an infinite-order symmetry. In other words, the shape necessarily produces non-periodic arrangements. This addresses a particularly demanding version of the three-dimensional Einstein problem: finding one shape that forces aperiodicity purely through its geometry.
The tile itself is geometrically quite interesting. It begins with a seven-cube chair: a $2\times2\times2$ cube with one corner cube removed. Its 24 exposed unit-square panels are modified with very small square-pyramid protrusions and indentations. These features act like a physical encoding of matching rules: neighboring tiles can only fit together in certain configurations. The resulting object is a rational polyhedral $3$-ball, meaning that it is topologically equivalent to a solid ball and its vertices have rational coordinates. Importantly, the construction does not impose external matching rules—the restrictions arise entirely from the shape itself.
The central mechanism is a hierarchical substitution structure. Eight appropriately rotated copies of the chair form a chair twice as large, and this process can be repeated indefinitely. Thus each individual tile belongs to a uniquely determined sequence of increasingly large “supertiles” with scales $2,4,8,\ldots,2^n$. If a translation were a symmetry of the tiling, it would have to remain a symmetry after passing to every larger scale. But the hierarchy forces the translation vector to be repeatedly halved; consequently the only possible translation is $0$. Formally, the authors establish $\operatorname{Per}(T)={0}$ and $|\operatorname{Sym}(T)|\leq24$ for every tiling $T$.
A particularly notable aspect is the extensive computer-assisted and formally verified proof. The authors enumerate possible configurations exactly rather than relying on numerical approximations. For example, $2{,}388$ candidate contact poses are reduced to exactly $44$ legal contacts, while other stages involve thousands of possible configurations and hundreds of thousands of collision checks. These computations were independently replayed in two Python implementations, while the finite statements and logical assembly were checked in Lean 4, using exact integers and rational arithmetic rather than floating-point calculations. The paper is explicitly presented as a proof submission pending refereeing, so its result should currently be regarded as a new preprint rather than an established peer-reviewed theorem.
Key takeaways
- Main result: A single three-dimensional polyhedral tile $Q$ is shown to tile $\mathbb{R}^3$ while forcing aperiodicity.
- The tile is called Chair44 (R44) and is based on a seven-cube chair.
- Its small geometric bumps and dents encode matching constraints through shape alone.
- Every tiling has no nonzero translational period:
Per(T)={0}.\operatorname{Per}(T)=\{0\}.
- Every tiling has a finite symmetry group:
∣Sym(T)∣≤24.|\operatorname{Sym}(T)|\leq24.
- Every tiling is homochiral: all copies have the same handedness.
- Each tile belongs to a unique hierarchy of supertiles with scales
20,21,22,….2^0,2^1,2^2,\ldots.
- The proof's key idea is recognizability + hierarchical substitution + period halving.
- The finite contact structure contains exactly 44 legal contacts after eliminating $2{,}388$ candidates.
- The computational part uses exact arithmetic, avoiding floating-point uncertainty.
- The finite enumerations and logical proof assembly are formally checked in Lean 4, modulo explicitly identified compiler hooks.
- The paper connects modern aperiodic tilings, combinatorics, discrete geometry, substitution systems, and formal proof.
- The work is currently a September 2026 arXiv proof submission, not yet a peer-reviewed publication.
Read the full paper on arXiv