Periodic tiling conjecture fails in dimension 3 (OpenAI claim, Lean-checked)

Your AI and this story

Key facts

• Claim (abstract, verbatim): ‘We construct a finite translational tile in ℤ³ that admits tilings but no fully periodic tiling. Its unit-cube thickening has the same property in ℝ³, even when arbitrary real translations are allowed. This gives a negative resolution of the periodic tiling conjecture in dimension three.’
• Minimality (paper, §1): ‘For lattice tilings, dimension three is the smallest possible dimension for this conclusion’, by Newman’s theorem for ℤ and Bhattacharya’s for ℤ² (Amer. J. Math. 2020). The Lean statement proves this too (IsLeast … 3), with its own proofs that finite tiles of ℤ and ℤ² have periodic tilings
• Method (paper): Greenfeld and Tao disproved the conjecture ‘in sufficiently large dimension’, and the new proof ‘follows this general strategy and the p-adic Sudoku formulation of Greenfeld and Tao’, with a new encoding that keeps the finite group factor cyclic so that ℤ² × ℤ/Qℤ is a quotient of ℤ³. The construction uses a prime p > 200 and ‘No practical bound on the size of the finite construction is required’. The tile is not claimed to be connected, and the result is about full periodicity, not every single period
• Lean: comparator challenge PeriodicTilingThree.lean, theorem periodic_tiling_counterexample_and_minimality (the ℤ³ tile, the a.e. tiling of ℝ³ by its thickening with no lattice-periodic translation set, and minimality of dimension 3). Accepted in oai-math-revised’s Comparator run of 25–26 Oct; acceptance checks the proof against the challenge statement, not the statement against the paper
• Reception: Gil Kalai (7 Oct) lists it among release results tied to his blog, saying it gives a tile ‘that admits no fully periodic tiling, reaching the smallest possible dimension for the lattice problem’. Chaim Goodman-Strauss (Museum of Mathematics) told Quanta (9 Oct) it has some novel mathematical ideas but is ‘unnecessarily difficult to read… I figure this is pretty representative across the corpus’, and that it is not remotely close to publishable form by traditional norms
• Follow-up: Erik D. Demaine and Stefan Langerman, ‘Tiling 3D by Translates of a Single Polycube is Undecidable’ (arXiv 2610.12392, 8 Oct): co-RE-completeness for one face-connected polycube, using ‘a cyclic encoding adapted from OpenAI’s 3D aperiodic tile’. Their repository says the cyclic gadgets are ‘adapted and reproved from Sections 3–6’ of OpenAI’s paper, and that it ‘does not substitute the periodic-only descent in Section 7’. The proof is in Lean, and ‘We made heavy use of AI to find, write, and formalize the proof’ (GPT 6.1 Sol, GPT 6 Astra, Claude Sonnet 5.5, Claude Opus 5.5, Claude Fable 5.1)
• Related results: Tan and Zhang (arXiv 2609.26576, 22 Sept; ChatGPT Codex used ‘for mathematical exploration, proof drafting and checking’) prove that every finite tile of ℤᵈ with 2q (q an odd prime) or 9 cells has a fully periodic tiling. Tsiokos’s Chair44 (September) is a different kind of result: a strongly aperiodic 3D monotile whose copies may be rotated and reflected, while the periodic tiling conjecture allows translations only
• Size: a YouTube explainer (Myren Eario, 7 Oct, about 16,500 views) presents Claude Sonnet 5.5’s rough estimates of how big the tile is. They come from asking a model to read the paper and are not in it