Papers With

← All papers
First page of Tiling 3D by Translates of a Single Polycube is Undecidable

Tiling 3D by Translates of a Single Polycube is Undecidable

Erik D. Demaine, Stefan Langerman

cs.CG Oct 8, 2026 · v1 math.CO math.MG
formalization mathlib combinatorics ai-agents
Read PDF arXiv abstract Code
TL;DR
The full undecidability proof for single-polycube translational tiling is formalized in Lean 4 on Mathlib, building on the lean-wang Wang-tiling formalization.
Abstract
We prove co-RE-completeness, and thus undecidability, of the following problem: given a single (connected) polycube, decide whether it tiles 3D Euclidean space by translations. We reduce from Wang tiling using the decorated two-prime Sudoku construction of Greenfeld and Tao and a cyclic encoding adapted from OpenAI's 3D aperiodic tile, and apply a reduction of Kim to make the prototile connected (via faces). Dimension three is optimal: translational monotiling is known to be decidable in $\mathbb{Z}^2$ and for a single (possibly disconnected) polyomino in $\mathbb{R}^2$.
Problem

Whether a single connected polycube tiles 3D space by translations had no known decidability status. Dimension two is known to be decidable for a single prototile, and the previous 3D undecidability record used two prototiles.

Approach

The proof reduces from Wang tiling via Greenfeld and Tao's decorated two-prime Sudoku construction. It then uses a cyclic encoding adapted from OpenAI's 3D aperiodic tile, and applies Kim's reduction to make the prototile face-connected. The entire proof was found, written, and formalized with heavy LLM assistance. It was verified in Lean 4 using Mathlib and lean-wang, with a short Abstract.lean file stating the trusted definitions and theorems.

Results

Translational tiling of Z^3 and R^3 by a single connected polycube is co-RE-complete and hence undecidable, which makes three the optimal dimension. The Lean proof depends only on Lean's three standard axioms.