HEXAGONbeta

No lattice tiling of Z35\mathbb{Z}^{35} or Z805\mathbb{Z}^{805} by Lee balls of radius three

A mix of human-written and AI-generated textHuman understanding: some partsmath.CO — Combinatoricsmath.MG — Metric Geometrymath.NT — Number Theorycs.IT — Information Theory

Contributed by Deep Bhattacharjee ↗, Ushashi Bhattacharya ↗

Version 1 / Oct 17, 2026 / CC BY 4.0

Abstract

We prove that there is no lattice tiling of Z35\mathbb{Z}^{35} or of Z805\mathbb{Z}^{805} by Lee balls of radius three. These were the only cases left open by Xiao and Zhou among the Lee balls of dimension at least three and radius at least two with fewer than 2302^{30} points, so the lattice Golomb--Welch conjecture holds for all of them.

Provenance statement

The proofs, the text, the figures, the Lean 4 formalisation and the C, C++, Python, Julia and shell programs were carried out by Deep Bhattacharjee with the help of AI assistance (Claude, Anthropic) in the Claude Code environment. The reduction of a lattice tiling to a group-ring equation follows Zhang and Zhou and Xiao and Zhou, and the paper credits them; the new steps are the constant term modulo 29^2 for n = 805 and the joint projection to Z/71 x Z/29 through dual numbers with the circulant systems for n = 35. Both theorems are proved in Lean 4 with Mathlib (GolombWelch.golomb_welch_35 and GolombWelch.golomb_welch_805), depending only on the axioms propext, Classical.choice and Quot.sound, with no sorry, native_decide or added axiom; the finite computations in F_29, F_71 and Z/841 are checked by the kernel, and every finite quantity of the paper is recomputed by programs in at least two languages. No statement rests on a floating-point computation. The paper does not prove the Golomb-Welch conjecture: it settles two cases of its lattice form, and tilings that are not lattice tilings are not covered because 59711 and 696845031 are not prime. Both authors approved the final version. Tools used: Anthropic - Claude (Claude Code); Lean community - Lean 4 (v4.34.1) with Mathlib; C; C++; Python; Julia; shell. arXiv identifier: none (not posted on arXiv). Formalization: https://github.com/creelie/refactored-waddle/blob/main/lean/GolombWelch.lean (archived at Zenodo, release v1.0.0: https://doi.org/10.5281/zenodo.23398805)
AI provenance filesAI_PROVENANCE_GolombWelchRadiusTh.md · 4 KB

Tools used

Anthropic
Claude CodeVersion Opus 5.5 Ultracode

References

  1. D. Bhattacharjee, Establishing equivariant class [O][O] for hyperbolic groups , Asian Res. J. Math. 18 (2022), no. 11, 362--369, doi:10.9734/arjom/2022/v18i11615 (https://doi.org/10.9734/arjom/2022/v18i11615).DOI
  2. D. Bhattacharjee and U. Bhattacharya, No lattice tiling of Z35\mathbb{Z}^{35} or Z805\mathbb{Z}^{805} by Lee balls of radius three: Lean formalization and programs , Zenodo, 2026, doi: (https://doi.org/\zenodoID).link
  3. D. Bhattacharjee, U. Bhattacharya and S. Bhattacharya, The sphere packing problem in dimension 44 , Preprints.org, 2026. doi:10.20944/preprints202606.0856.v11 (https://doi.org/10.20944/preprints202606.0856.v11).DOI
  4. D. Bhattacharjee, U. Bhattacharya and S. Bhattacharya, The sphere packing problem in dimension 77 , Preprints.org, 2026. doi:10.20944/preprints202606.1534.v9 (https://doi.org/10.20944/preprints202606.1534.v9).DOI
  5. R. Dougherty and V. Faber, The degree-diameter problem for several varieties of Cayley graphs I: the abelian case , SIAM J. Discrete Math. 17 (2004), 478--519, doi:10.1137/S0895480100372899 (https://doi.org/10.1137/S0895480100372899).DOI
  6. S. W. Golomb and L. R. Welch, Perfect codes in the Lee metric and the packing of polyominoes , SIAM J. Appl. Math. 18 (1970), 302--317, doi:10.1137/0118025 (https://doi.org/10.1137/0118025).DOI
  7. S. Gravier, M. Mollard and C. Payan, On the non-existence of 33-dimensional tiling in the Lee metric , European J. Combin. 19 (1998), 567--572, doi:10.1006/eujc.1998.0211 (https://doi.org/10.1006/eujc.1998.0211).DOI
  8. P. Horak, Tilings in Lee metric , European J. Combin. 30 (2009), 480--489, doi:10.1016/j.ejc.2008.04.007 (https://doi.org/10.1016/j.ejc.2008.04.007).DOI
  9. P. Horak and B. F. AlBdaiwi, Diameter perfect Lee codes , IEEE Trans. Inform. Theory 58 (2012), 5490--5499, doi:10.1109/TIT.2012.2196257 (https://doi.org/10.1109/TIT.2012.2196257).DOI
  10. P. Horak and D. Kim, 50 years of the Golomb--Welch conjecture , IEEE Trans. Inform. Theory 64 (2018), 3048--3061, doi:10.1109/TIT.2017.2786675 (https://doi.org/10.1109/TIT.2017.2786675).DOI
Show all 21 referencesShow fewer references
  1. D. Kim, Nonexistence of perfect 22-error-correcting Lee codes in certain dimensions , European J. Combin. 63 (2017), 1--5, doi:10.1016/j.ejc.2017.01.007 (https://doi.org/10.1016/j.ejc.2017.01.007).DOI
  2. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language , in: Automated Deduction -- CADE 28, Lecture Notes in Comput. Sci. 12699, Springer, 2021, pp. 625--635, doi:10.1007/978-3-030-79876-5_37 (https://doi.org/10.1007/978-3-030-79876-5_37).DOI
  3. K. H. Leung and Y. Zhou, No lattice tiling of Zn\mathbb{Z}^n by Lee sphere of radius 22 , J. Combin. Theory Ser. A 171 (2020), 105157, doi:10.1016/j.jcta.2019.105157 (https://doi.org/10.1016/j.jcta.2019.105157).DOI
  4. The mathlib Community, The Lean mathematical library , in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, pp. 367--381, doi:10.1145/3372885.3373824 (https://doi.org/10.1145/3372885.3373824).DOI
  5. K. A. Post, Nonexistence theorems on perfect Lee codes over large alphabets , Inform. and Control 29 (1975), 369--380, doi:10.1016/S0019-9958(75)80005-2 (https://doi.org/10.1016/S0019-9958(75)80005-2).DOI
  6. C. Qureshi, On the non-existence of linear perfect Lee codes: the Zhang--Ge condition and a new polynomial criterion , European J. Combin. 83 (2020), 103022, doi:10.1016/j.ejc.2019.103022 (https://doi.org/10.1016/j.ejc.2019.103022).DOI
  7. M. Szegedy, Algorithms to tile the infinite grid with finite clusters , in: Proceedings of the 39th Annual Symposium on Foundations of Computer Science (FOCS 1998), IEEE, 1998, pp. 137--145, doi:10.1109/SFCS.1998.743437 (https://doi.org/10.1109/SFCS.1998.743437).DOI
  8. A. Xiao and Y. Zhou, On the lattice tilings by Lee balls: QQ-polynomials, group-ring equations, and a decision algorithm , arXiv:2610.19775 (https://arxiv.org/abs/2610.19775), 2026.arXiv
  9. T. Zhang and G. Ge, Perfect and quasi-perfect codes under the lpl_p metric , IEEE Trans. Inform. Theory 63 (2017), 4325--4331, doi:10.1109/TIT.2017.2685424 (https://doi.org/10.1109/TIT.2017.2685424).DOI
  10. T. Zhang and G. Ge, On linear diameter perfect Lee codes with distance 66 , J. Combin. Theory Ser. A 201 (2024), 105816, doi:10.1016/j.jcta.2023.105816 (https://doi.org/10.1016/j.jcta.2023.105816).DOI
  11. T. Zhang and Y. Zhou, On the nonexistence of lattice tilings of Zn\mathbb{Z}^n by Lee spheres , J. Combin. Theory Ser. A 165 (2019), 225--257, doi:10.1016/j.jcta.2019.02.008 (https://doi.org/10.1016/j.jcta.2019.02.008).DOI

Version history

  1. v1Submitted by Deep BhattacharjeeInitial depositCurrentOct 17, 2026