∑math20

Combinatorics · Result 155

A counterexample to periodic tiling in dimension three

1 paperLean

Constructs a finite translational tile in ℤ3 that tiles space but admits no fully periodic tiling, disproving the periodic tiling conjecture in the smallest possible lattice dimension. Its unit-cube thickening gives the same counterexample in ℝ3, even with arbitrary real translation vectors.

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 1

First page of A translational tile with no fully periodic tiling in dimension three

A translational tile with no fully periodic tiling in dimension three

OpenAI · September 23, 2026

We construct a finite translational tile in ℤ3 that admits tilings but no fully periodic tiling. Its unit-cube thickening has the same property in ℝ3, even when arbitrary real translations are allowed. This gives a negative resolution of the periodic tiling conjecture in dimension three.

Read PDF Download Source

Cite
@misc{OAI:A-translational-tile-with-no-fully-periodic-tiling-in-dimension-three-September-23-2026,
  author = {{OpenAI}},
  title = {{A translational tile with no fully periodic tiling in dimension three}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-translational-tile-with-no-fully-periodic-tiling-in-dimension-three-September-23-2026/paper.pdf}{OAI:A-translational-tile-with-no-fully-periodic-tiling-in-dimension-three-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The periodic-tiling question asks whether a finite tile that tiles a lattice must admit a periodic tiling. The formalized counterexample is a finite tile in \(\mathbb Z^3\) that tiles but has no complement invariant under a finite-index subgroup. Its unit-cube thickening also tiles \(\mathbb R^3\) almost everywhere but admits no fully periodic tiling, even with arbitrary real translation vectors. The result also establishes that dimension three is the least lattice dimension where this failure occurs.

Comparator links

ResultComparator statement
Aperiodic translational tile in dimension threePeriodicTilingThree.lean

Scope note on GitHub →