# AI provenance: Densest packings of two translates of a lattice in five dimensions

Authors: Deep Bhattacharjee (corresponding author, ORCID 0000-0003-0466-750X)
and Ushashi Bhattacharya (ORCID 0009-0002-2254-3914).

- Paper: https://github.com/creelie/D5/blob/main/preprintAndreanovKallusTwoPeriodicPackingD5/AndreanovKallusTwoPeriodicPackingD5.pdf
- Lean formalisation and code: doi:10.5281/zenodo.23387908 (release v2.0.0; all versions doi:10.5281/zenodo.23323366)
- Repository: https://github.com/creelie/D5

## Result

Let Λ ⊂ R^5 be a lattice and b ∉ Λ such that distinct points of
P = Λ ∪ (Λ + b) are at distance at least 2. The paper proves that
covol(Λ) ≥ 16√2, with equality for exactly five pairs (Λ, b) up to
congruence, whose point sets are √2 D5, √2 P1 (a layered packing of Leech)
and √2 P2 (the packing with Szöllősi's kissing configuration). So no packing
of unit balls whose centres form two translates of a lattice is denser than
the D5 lattice packing, and every Voronoi cell of such a packing has volume
at least 8√2. This proves the five-dimensional bound that Andreanov and
Kallus found numerically.

The proof has four steps:

- Section 2: a two-periodic set is encoded by the 6 × 6 Gram matrix J of a
  basis of Λ together with b; the packing condition cuts out a locally finite
  polyhedron R in the 21-dimensional space of such matrices.
- Proposition 3.2: by the concavity of log det Q and of the Schur complement
  of Q in J, every packing can be moved, without increasing det Q, to a vertex
  of R or to a point of an edge of R.
- Proposition 4.3: up to the integral symmetries, R has 34 vertices, whose
  cones have 80,695 extreme rays in 480 orbits, 25 of them unbounded edges.
  This finite table is the computational statement.
- Sections 5 and 6: the minimum 512 of det Q is attained only at five points,
  by a deep hole lemma in the plane, and the five configurations are
  identified and shown to be pairwise not congruent.

## Who did what

Deep Bhattacharjee chose the problem, directed the work, set the format and
the target journal (Discrete & Computational Geometry), and ran the
computations. Claude (Anthropic), used through Claude Code under his
direction, produced the following:

- the proofs;
- the Lean 4 formalisation and the certificate generators;
- the programs in C, C++, Julia, Python and shell;
- the figures;
- the LaTeX text of the paper.

No other AI system took part.

## How the result is checked

- **Lean 4 with Mathlib.** The theorem `D5.certificate` proves, for the 34
  vertices and the 480 representative edges of the certificate: that each
  vertex lies in R, its minimal vectors up to sign, the values of det J and
  det Q; along every representative edge, det J > 0 or det Q ≥ 512, with
  equality only at the listed points; for a bounded edge, the end point and
  the integral matrix carrying it to a listed vertex; for an unbounded edge,
  that it stays in R. Every step is checked by the kernel (`decide +kernel`;
  `native_decide` is not used). The theorem depends only on the standard
  axioms propext, Classical.choice and Quot.sound. There is no `sorry`,
  `admit` or added axiom.
- **Independent programs.** Four implementations, in C and C++ with
  multiprecision rationals, in Julia and in Python, re-check the whole
  certificate in exact arithmetic, including the rank conditions and the
  orbit decompositions. Four enumerations (a double description
  implementation, a reverse search and two further double description
  programs in C and Julia) recompute the extreme rays of all 34 cones and
  agree with the certificate.
- **Workflows.** Every pull request runs these checks, builds the Lean proof
  and builds the paper.

## What is not claimed

- The Lean proof is not a complete formal proof of Proposition 4.3. Three
  ingredients are not formalized: the rank conditions that make the vertices
  vertices and the listed rays extreme, the completeness of the lists of
  extreme rays, and the orbit decompositions. They rest on the exact
  computations of the independent programs. A formal certificate of
  completeness would have to treat every set of 20 independent minimal
  vectors of a vertex with up to 36 minimal vectors, and none was produced.
- The reduction to vertices and edges (Proposition 3.2), the closure argument
  and the equality case are proved by hand in the paper.
- The theorem covers packings whose centres form two translates of a lattice.
  Whether D5 is the densest packing of unit balls in R^5 remains open.
- Andreanov and Kallus (Discrete Comput. Geom. 63 (2020), 182–208) enumerated
  the locally optimal two-periodic packings in dimension 5, partly in
  floating-point arithmetic, and present the result as numerical; Cohn and
  Rajagopal (Discrete Comput. Geom. 76 (2026), 1660–1678) cite it. On
  15 October 2026 the authors searched arXiv and the web and found no earlier
  rigorous proof.