oai-math-revised beta

Browse › Convex and metric geometry › 090 Triangular-lattice optimality, long-range Riesz and Coulomb energies, and spherical logarithmic energy

An atomic certificate for triangular-lattice universal optimality

OpenAI · September 26, 2026

Lean

Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion

Edit NOTES.md · Existing issues · Source on GitHub

Abstract

We prove that the density-one triangular lattice minimizes the lower energy per particle for every nonnegative completely monotone function of squared distance, among all locally finite planar configurations of centered disk density one. The comparison includes infinite energies. The proof constructs sharp Gaussian Fourier minorants using an atomic interpolation certificate.

If the PDF does not display here, open it directly: Open PDF.

Notes

No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.

Automatically collected notes (unreviewed)

work in progress

Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.

Formalization

  • OpenAI math release, Lean scope note for family 090 (lean/docs/090.md, release of 2026-10-06). Describes the release's Lean formalization of this paper's Theorem 1.1 (universal energy minimum) and the sharp Gaussian minorants, including the atomic construction, with comparator statements TriangularEnergy.lean, AtomicGaussian.lean and TriangularGaussian.lean. [family-level]
  • Xavier Callens, triangular-universal-optimality-lean (GitHub repository, rebuild dated 2026-10-11). Lean 4 corollaries (Riesz energies, other densities, a CKMRV-style formulation, open-disk variant) derived from the release theorem OAI.AtomicTriangular.universal_energy_minimum; the repository describes them as conditional corollaries, says the liminf "lower energy" is a weaker notion, and states it is not peer reviewed. [AI-generated per source]

Digests and expositions

News and blogs

Elsewhere

Independent sites; their content is not reviewed here.

Cite

@misc{OAI:An-atomic-certificate-for-triangular-lattice-universal-optimality-September-26-2026,
  author = {{OpenAI}},
  title = {{An atomic certificate for triangular-lattice universal optimality}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-atomic-certificate-for-triangular-lattice-universal-optimality-September-26-2026/paper.pdf}{OAI:An-atomic-certificate-for-triangular-lattice-universal-optimality-September-26-2026}},
  year = {2026}
}

From OpenAI's README for this paper:

Verification

The exact finite checker uses only the Python 3 standard library:

python3 -I -B verification/check_certificate.py

A successful run exits zero without output. Do not use -O or -OO. See verification/README.md for its finite scope and for the distinction between static certificate metadata and an execution record.

Lean formalization

OpenAI provides Lean files for this family: lean/docs/090.md. The Lean statements have not been checked by people against the paper's claims.

Family 090: Triangular-lattice optimality, long-range Riesz and Coulomb energies, and spherical logarithmic energy

Proves that the triangular lattice minimizes the lower limit of energy per particle for every nonnegative completely monotone potential of squared distance among locally finite planar configurations of centered-disk density one. It also minimizes unit-background renormalized Riesz energies for $0\lt s\lt 2$ and Coulomb energy, resolving Sandier–Serfaty and the two-dimensional Brauchart–Hardin–Saff conjecture on the linear term of optimal spherical logarithmic energy.

Other papers in this family: