HEXAGONbeta

Densest packings of two translates of a lattice in five dimensions

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

Contributed by Deep Bhattacharjee ↗, Ushashi Bhattacharya ↗

Version 1 / Oct 22, 2026 / CC BY 4.0

Abstract

We prove that no packing of unit balls in R5\R^5 whose centres form two translates of a lattice is denser than the D5D_5 lattice packing. Up to congruence exactly three such packings attain this density: 2 D5\sqrt2\,D_5, a layered packing of Leech, and the packing with Szöllősi's kissing configuration.

Provenance statement

Deep Bhattacharjee chose the problem and directed the work. Claude (Anthropic), through Claude Code, carried out the searches and computations, wrote the checking programs and the Lean 4 proofs and drafted the paper. A theorem on a stated case: two translates of a lattice in five dimensions. The completeness of the ray lists rests on an exact computer enumeration. The proofs are written out in the paper; the programs and their outputs are in the release. Both authors approved the final version. Code and data: release v2.0.0, https://github.com/creelie/D5/releases/tag/v2.0.0.
AI provenance filesAI_PROVENANCE_AndreanovKallusTwoPeriodicPackingD5.md · 5 KB

Tools used

Anthropic
Claude CodeVersion Opus 5.5 Ultracode

References

  1. A. Andreanov and Y. Kallus, Locally optimal 2-periodic sphere packings , Discrete Comput. Geom. 63 (2020), 182--208. 10.1007/s00454-019-00150-6DOI
  2. D. Avis and K. Fukuda, A pivoting algorithm for convex hulls and vertex enumeration of arrangements and polyhedra , Discrete Comput. Geom. 8 (1992), 295--313. 10.1007/BF02293050DOI
  3. D. Bhattacharjee and U. Bhattacharya, Densest packings of two translates of a lattice in four dimensions , preprint, 2026, https://github.com/creelie/eD424/blob/main/preprintMusin24CellConjectureTwoTranslates/Musin24CellConjectureTwoTranslates.pdf; Lean formalization, programs and certificates at Zenodo, 10.5281/zenodo.23387006DOI
  4. D. Bhattacharjee and U. Bhattacharya, Densest packings of two translates of a lattice in five dimensions: Lean formalization, programs and certificate , Zenodo, 2026.
  5. J. W. S. Cassels, An Introduction to the Geometry of Numbers , Grundlehren Math. Wiss. 99, Springer, Berlin, 1959. 10.1007/978-3-642-62035-5DOI
  6. H. Cohn and I. Rajagopal, Variations on five-dimensional sphere packings , Discrete Comput. Geom. 76 (2026), 1660--1678. 10.1007/s00454-026-00841-xDOI
  7. J. H. Conway and N. J. A. Sloane, What are all the best sphere packings in low dimensions? , Discrete Comput. Geom. 13 (1995), 383--403. 10.1007/BF02574051DOI
  8. J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups , 3rd ed., Grundlehren Math. Wiss. 290, Springer, New York, 1999. 10.1007/978-1-4757-6568-7DOI
  9. U. Fincke and M. Pohst, Improved methods for calculating vectors of short length in a lattice, including a complexity analysis , Math. Comp. 44 (1985), 463--471. 10.1090/S0025-5718-1985-0777278-8DOI
  10. K. Fukuda and A. Prodon, Double description method revisited , in: Combinatorics and Computer Science, Lecture Notes in Comput. Sci. 1120, Springer, Berlin, 1996, 91--111. 10.1007/3-540-61576-8_77DOI
Show all 18 referencesShow fewer references
  1. A. Korkine and G. Zolotareff, Sur les formes quadratiques positives , Math. Ann. 11 (1877), 242--292. 10.1007/BF01442667DOI
  2. J. Leech, Five dimensional non-lattice sphere packings , Canad. Math. Bull. 10 (1967), 387--393. 10.4153/CMB-1967-037-5DOI
  3. The mathlib Community, The Lean mathematical library , in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, New York, 2020, 367--381. 10.1145/3372885.3373824DOI
  4. 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, Cham, 2021, 625--635. 10.1007/978-3-030-79876-5_37DOI
  5. A. Schürmann, Computational Geometry of Positive Definite Quadratic Forms , Univ. Lecture Ser. 48, Amer. Math. Soc., Providence, RI, 2009. 10.1090/ulect/048DOI
  6. F. Szöllősi, A note on five-dimensional kissing arrangements , Math. Res. Lett. 30 (2023), 1609--1615. 10.4310/MRL.2023.v30.n5.a13DOI
  7. G. Voronoi, Nouvelles applications des paramètres continus à la théorie des formes quadratiques. Premier mémoire. Sur quelques propriétés des formes quadratiques positives parfaites , J. Reine Angew. Math. 133 (1908), 97--178. 10.1515/crll.1908.133.97DOI
  8. G. M. Ziegler, Lectures on Polytopes , Grad. Texts in Math. 152, Springer, New York, 1995. 10.1007/978-1-4613-8431-1DOI

Version history

  1. v1Submitted by Deep BhattacharjeeInitial depositCurrentOct 22, 2026