The optimal order of convex-body covering density

2 papersLean

Determines the optimal worst-case covering density as \(\Theta(n\log n)\), for both lattice and unrestricted translative coverings. Every convex body in ℝⁿ, n ≥ 2, admits a lattice covering of density at most \(Cn\log n\); centrally symmetric examples in every sufficiently large dimension require at least \(cn\log n\) even without the lattice restriction, for absolute \(c,C\gt 0\).

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

A single-lattice covering bound of order n log n

OpenAI · September 23, 2026

Every convex body in ℝⁿ, n ≥ 2, admits a covering by translates along one full-rank lattice with density at most \(Cn\log n\), for an absolute constant C. No symmetry or boundary regularity is assumed.

Read PDF Download Source

Cite

@misc{OAI:A-single-lattice-covering-bound-of-order-n-log-n-September-23-2026,
  author = {{OpenAI}},
  title = {{A single-lattice covering bound of order $n\log n$}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-single-lattice-covering-bound-of-order-n-log-n-September-23-2026/paper.pdf}{OAI:A-single-lattice-covering-bound-of-order-n-log-n-September-23-2026}},
  year = {2026}
}

Translative covering densities of order n log n

OpenAI · September 23, 2026

For every sufficiently large dimension n, we construct a centrally symmetric convex body whose translative covering density exceeds \(c n\log n\), where c > 0 is absolute. This disproves the existence of a universal linear upper bound and matches the order of Rogers' upper bound.

Read PDF Download Source

Cite

@misc{OAI:Translative-covering-densities-of-order-n-log-n-September-23-2026,
  author = {{OpenAI}},
  title = {{Translative covering densities of order $n\log n$}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Translative-covering-densities-of-order-n-log-n-September-23-2026/paper.pdf}{OAI:Translative-covering-densities-of-order-n-log-n-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalized result gives an absolute constant \(C>0\) such that every convex body \(K\subset\mathbb R^n\), \(n\ge2\), admits a covering by translates along one full-rank lattice \(L\) with density \(|K|/\mathrm{covol}(L)\le Cn\log n\). The covering is exact, and no symmetry, boundary regularity, or volume normalization is assumed.

The formalization determines the order of the largest covering density in dimension \(n\). For all sufficiently large \(n\), the suprema of translative covering density and lattice covering density are each bounded above and below by absolute positive multiples of \(n\log n\), both over all convex bodies and over centrally symmetric convex bodies.

Comparator links

Result	Comparator statement
Single-lattice covering bound	SingleLatticeCovering.lean
Optimal order for translative and lattice covering-density suprema	CoveringDensity.lean

Scope note on GitHub →