The optimal order of convex-body covering density
The optimal order of convex-body covering density concerns the largest density needed to cover Rn by translates of a convex body. Rogers proved in 1957 that every convex body admits a translative covering of density at most n log n + n log log n + 5n, and the best lattice bounds remained weaker. Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math), dated 23 September 2026, claim that the worst-case density is of order n log n for lattice and for unrestricted translative coverings alike. The collection includes a Lean formalization of both claims. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introductions of the manuscripts:
- Rogers' translative bound may use a finite union of lattice cosets; Fejes Tóth obtained the same leading density with O(log n) cosets of one lattice. For a single lattice, Rogers proved nlog2 log n + O(1), Ordentlich, Regev and Weiss the universal bound O(n2), and Li and Liu n log n (log log n)10/3 + o(1), with a later improvement of the exponent of log log n.
- Li and Liu also gave centrally symmetric bodies, in every large dimension, whose lattice covering density is at least cn log n. Naszódi recorded the question whether a universal linear bound Cn holds for translative coverings.
The original results
- Claim (single lattice). Theorem 1.1 of A single-lattice covering bound of order n log n states that there is an absolute constant C such that every convex body K ⊂ Rn, n ≥ 2, is covered by its translates along one full-rank lattice with density at most Cn log n, with no symmetry or boundary regularity assumed. The manuscript states that this removes the iterated-logarithmic loss in Li and Liu's bound.
- Method, as described: the proof develops Li and Liu's horizontal–vertical framework and binary correction, controls section volumes with the pointwise Gaussian marginal theorem of Eldan and Klartag, and uses the lattice mean-hole method of Rogers and Schmidt in the form of Ordentlich, Regev and Weiss for one horizontal lattice.
- Claim (translative lower bound). Theorem 1.1 of Translative covering densities of order n log n states that there are absolute constants c > 0 and n0 such that, for every n ≥ n0, some centrally symmetric convex body has translative covering density greater than cn log n. The manuscript states that this answers Naszódi's linear-bound question negatively and, with Rogers' bound, shows that the supremum of covering density has order n log n; the bodies may be taken to be centrally symmetric rational polytopes.
- Sources (openai/math repository, commit
1581d4c): A single-lattice covering bound of order n log n and Translative covering densities of order n log n. - Formalization, as described by the repository. The scope note states that the formalization proves the single-lattice bound Cn log n for every convex body, and that, for all sufficiently large n, the suprema of translative and of lattice covering density are bounded above and below by absolute multiples of n log n, over all convex bodies and over centrally symmetric ones. The Comparator statements are
SingleLatticeCovering.leanandCoveringDensity.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full", noting that the lower bound for centrally symmetric bodies is stated for the translative supremum as well, hence for the lattice one. It records sandboxed Comparator passes for SingleLatticeCovering and CoveringDensity. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-09 | S. Kominers, Multi-coverings by lattice translates of convex bodies, Hexagon 2610.00165v1 | Extension | States that for every convex body K ⊂ Rn, every 0 < ε < 1 and every prescribed density ρ ≥ Aεn log n, there is an arrangement of translates of K along one lattice with mean multiplicity exactly ρ and multiplicity at least ρ − ερ everywhere; consequently lattice k-fold coverings exist with density at most the larger of (1 + ε)k and Cεn log n. A version with a common covolume holds simultaneously for up to exp{nc0} bodies with a common covariance matrix. The abstract states that the proof builds on OpenAI's horizontal–vertical construction for single-lattice coverings. | Hexagon record, version 1. |
| 2026-10-10 | cert-machine, openai/math lane K | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the SingleLatticeCovering solution (751 s, run 38019899278) and the CoveringDensity solution (1,031 s, run 38051470892). The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list SingleLatticeCovering or CoveringDensity, so the challenges were accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee review rank_406 (translative manuscript) in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap. The reviewer states that it read every section line by line and re-derived the main estimates, without checking external citations beyond their stated use. Its one minor note is that the corollary on the order of the lattice supremum relies on the companion single-lattice theorem, which this manuscript does not verify; the main theorem and the translative statements do not depend on it. | Part of an audit that its repository describes as a complete review of the collection's manuscripts without a Lean formalization; this manuscript is in its results table. The reviews are published under CC BY 4.0. |
Notes
- The earlier covering bounds and the lattice lower bound for centrally symmetric bodies are due to the authors named in the Background section, as recounted by the manuscripts.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.