Tiling 3D by Translates of a Single Polycube is Undecidable

1 Introduction

• The problem asks whether copies of k finite subsets of Z^d can cover Z^d without overlaps, and for which k and d this is decidable.The paper proves undecidability for k = 1 and d = 3.Source: §1 · p. 1
• The result reduces the 3D prototile count to one, the minimum possible, from the previous record of two.The first 3D undecidability result used six prototiles.Source: §1 · p. 1
• Dimension three is minimal for undecidability with one prototile, since algorithms are known for the corresponding 2D problem.The cited 2D results are [Bha20] [GT21].Source: §1 · p. 1
• Tiling Z^3 by translations of one finite connected subset is co-RE-complete, and tiling R^3 by one finite connected polycube is likewise co-RE-complete.Both problems are therefore undecidable.Source: §1 · p. 1
• The paper’s connectedness condition for polycubes means that constituent unit cubes are face-adjacent.Connectivity of the lattice subset is defined by lattice adjacency.Source: §1 · p. 1

2 Proof Overview

• A computable construction maps each finite Wang tile set T to a finite connected set F_T in Z^3 that tiles exactly when T tiles Z^2.Wang tiles are edge-colored unit squares, with touching colors required to match.Source: §2 · p. 2
• Greenfeld and Tao reduce Wang tiling to a Sudoku array whose fixed-width columns obey integer-slope line rules.Symbols encode Wang tiles and two integers whose powers of two fixed distinct primes encode the simulated plane’s coordinates.Source: §2 · pp. 2–3
• The adapted cyclic encoding uses prototiles and a shared translation set to enforce Wang constraints and both nonconstant-column conditions.Forbidden symbol combinations produce overlaps or gaps; the target is Z^2 × (Z/mZ).Source: §2 · p. 3
• OpenAI’s stacking construction combines the preceding family into one prototile, enlarging m while preserving tileability.The construction is based on an earlier Greenfeld and Tao construction.Source: §2 · p. 3
• The quotient-to-Z^3 reduction forces alignment to a scaled grid and repetition every m grid steps in the z direction.Matching bumps and dents enforce these constraints.Source: §2 · p. 3
• Kim’s connectedness reduction scales the prototile and links lattice points with thin corridors, using bumps and dents to force alignment.It preserves dimension, prototile count, and tileability.Source: §2 · p. 3

3.1 Prototiles

• The formalization treats a prototile as a finite list of points in Z3, so it can be supplied as algorithmic input.Repeated points are immaterial.Source: §3.1 · p. 4

3.2 Connectivity

• A prototile is connected when every pair of its points is joined by a path of adjacent points inside it.Adjacency means L1 distance 1.Source: §3.2 · p. 4

3.3 Tiling Z3

• A prototile tiles Z3 when some set of translations covers every lattice point exactly once, with no periodicity or finiteness requirement on that set.The translation set is not required to be periodic or finite.Source: §3.3 · p. 4

3.4 Main Theorem for Z3

• For connected prototiles, deciding whether a prototile tiles Z3 is co-RE-complete: non-tilers are recursively enumerable, and every co-RE problem reduces to the question.The theorem proof is a single call to a theorem in AbstractBridge.lean.Source: §3.4 · p. 5

3.5 Tiling R3

• The R3 definition uses the union of closed unit cubes at the prototile points and allows arbitrary real translations, requiring unique coverage almost everywhere.The almost-everywhere condition allows cubes to share boundaries.Source: §3.5 · p. 5

3.6 Main Theorem for R3

• The Lean 4 formalization establishes co-RE-completeness and undecidability for tiling Z3 and R3 by a single connected polycube.The authors say a reader can check the definitions and theorem statements in Abstract.lean; Lean verifies their proofs using only three standard axioms.Source: §3 · pp. 3–4, §3.6 · p. 5
• Tiling R3 by translations of the solid body of one finite connected polycube is co-RE-complete and therefore undecidable.The paper states that four Lean theorems establish Theorem 1.1.Source: §3.6 · p. 5

• The paper is not a complete human-readable account of the proof; it presents the problem, main intuition, and precise theorem statements.The authors say they intend to expand the paper with further human-readable explanations.Source: §4 · pp. 5–6
• The proof’s rigor comes from its Lean formalization rather than from the paper’s text.Source: §4 · p. 6
• A longer LLM-generated technical article and the complete Lean code provide the construction and proof details.Both are available in the repository.Source: §4 · p. 6