On the Lattice Tilings by Lee Balls: Q-Polynomials, Group-Ring Equations, and a Decision Algorithm
Ang Xiao, Yue Zhou
math.CO
Oct 14, 2026 · v1
TL;DR
All results except those resting on Maple computations are formalized and machine-checked in Lean 4 with Mathlib, using only standard axioms.
Abstract
More than 50 years ago, Golomb and Welch conjectured that no tilings of $\mathbb{Z}^n$ by Lee balls of radius $r$ exist for $n \geq 3$ and $r \geq 2$. This conjecture remains open even under the additional assumption that the tiling is a lattice tiling. In general, there are two known effective approaches to the lattice case which are based on symmetric polynomials and on the arithmetic of group-ring equations, respectively. In this paper, we develop both approaches. First, we determine all coefficients of the Q-polynomials associated with Lee balls; previously, only leading coefficients and certain special cases were known. Second, for arbitrary radii, we give necessary and sufficient conditions for the existence of lattice tilings by Lee balls in terms of group-ring equations, extending earlier results for radii $r=2$ and $3$. We then derive new necessary conditions for such tilings. For every radius $3\le r\le 50$, we prove that the set of dimensions for which no lattice tiling exists has positive density in \(\mathbb{Z}^+\). We also give an algorithm that combines the available necessary conditions and apply it to all pairs $(n,r)$ for which the corresponding Lee ball of radius $r$ and dimension $n$ has size less than $2^{30}$. Among these $1{,}358$ pairs, the combined method excludes $1{,}356$, leaving only $(n,r)=(35,3)$ and $(805,3)$.
Problem
The Golomb–Welch conjecture states that no tilings of Z^n by Lee balls of radius r exist for n ≥ 3 and r ≥ 2. It remains open even for lattice tilings. The two known effective approaches to the lattice case use symmetric polynomials and group-ring equations.
Approach
The authors compute all coefficients of the Q-polynomials associated with Lee balls. For arbitrary radii, they give necessary and sufficient conditions for lattice tilings in terms of group-ring equations, and from these derive new necessary conditions. An algorithm combines the available necessary conditions. The proofs are machine-checked in Lean 4 with Mathlib, except steps that rely on Maple computations.
Results
For each radius 3 ≤ r ≤ 50, the set of dimensions with no lattice tiling has positive density. Among the 1,358 pairs (n,r) whose Lee ball has size below 2^30, the algorithm excludes all but (35,3) and (805,3).