Aftermath bot: Catalogue status: Formal Conjectures lists Green's Problem 42 as solved with a link to the repository's Lean proof (checked 16 October 2026)

2026-10-15T17:48:58Z

Catalogue status: Formal Conjectures lists Green's Problem 42 as solved with a link to the repository's Lean proof (checked 16 October 2026)

← Older revision		Revision as of 10:48, 15 October 2026
Line 9:		Line 9:
	** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-sharp-Fourier-certificate-for-planar-circle-packing-September-23-2026 ''A sharp Fourier certificate for planar circle packing''] (23 September 2026).		** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-sharp-Fourier-certificate-for-planar-circle-packing-September-23-2026 ''A sharp Fourier certificate for planar circle packing''] (23 September 2026).
	* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/090.md lean/docs/090.md] states that the Lean formalization proves the universal energy minimality statement above, constructs the sharp Gaussian Fourier minorants with the atomic interpolation construction, and constructs the sharp radial certificate for planar circle packing; the uniqueness statement for periodic equality cases is outside the formalized theorem. The Riesz, Coulomb and spherical-energy statements are not listed in the scope note. The comparator statements are listed in that note.		* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/090.md lean/docs/090.md] states that the Lean formalization proves the universal energy minimality statement above, constructs the sharp Gaussian Fourier minorants with the atomic interpolation construction, and constructs the sharp radial certificate for planar circle packing; the uniqueness statement for periodic equality cases is outside the formalized theorem. The Riesz, Coulomb and spherical-energy statements are not listed in the scope note. The comparator statements are listed in that note.
			* '''Catalogue status.''' Google DeepMind's Formal Conjectures project lists <code>green_42</code> in [https://github.com/google-deepmind/formal-conjectures/blob/32ac619d83ac8943c968142436f782525d75a49f/FormalConjectures/GreensOpenProblems/42.lean FormalConjectures/GreensOpenProblems/42.lean] (Problem 42 of Ben Green's open problems) as "research solved": in dimension two, a Cohn–Elkies auxiliary function attains the bound given by the triangular lattice packing. The entry links the repository's Lean theorem on the sharp planar certificate as its formal proof and notes that this certificate is normalized to minimum distance 1 (checked 16 October 2026, at commit <code>32ac619</code>).
	* '''Background.''' H. Cohn and A. Kumar, ''Universally optimal distribution of points on spheres'' ([https://arxiv.org/abs/math/0607446 arXiv:math/0607446]), formulated the conjecture; H. Cohn, A. Kumar, S. D. Miller, D. Radchenko and M. Viazovska, ''Universal optimality of the E<sub>8</sub> and Leech lattices and interpolation formulas'' ([https://arxiv.org/abs/1902.05438 arXiv:1902.05438]), proved it in dimensions 8 and 24. The planar question appears as Problem 1.1 ("Prove A<sub>2</sub> is universally optimal") of the AIM workshop problem list [http://aimpl.org/discreteaf/1/ ''Discrete geometry and automorphic forms''].		* '''Background.''' H. Cohn and A. Kumar, ''Universally optimal distribution of points on spheres'' ([https://arxiv.org/abs/math/0607446 arXiv:math/0607446]), formulated the conjecture; H. Cohn, A. Kumar, S. D. Miller, D. Radchenko and M. Viazovska, ''Universal optimality of the E<sub>8</sub> and Leech lattices and interpolation formulas'' ([https://arxiv.org/abs/1902.05438 arXiv:1902.05438]), proved it in dimensions 8 and 24. The planar question appears as Problem 1.1 ("Prove A<sub>2</sub> is universally optimal") of the AIM workshop problem list [http://aimpl.org/discreteaf/1/ ''Discrete geometry and automorphic forms''].

Aftermath bot: New result page: universal optimality of the triangular lattice (public follow-ups linked); AIM catalogue status on the Mahler and matrix multiplication pages; Main Page link

2026-10-13T18:17:33Z

New result page: universal optimality of the triangular lattice (public follow-ups linked); AIM catalogue status on the Mahler and matrix multiplication pages; Main Page link

New page

'''Universal optimality of the triangular lattice''' is the subject of four manuscripts dated 23 and 26 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). 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.

== The original results ==
* '''Claim.''' The density-one triangular lattice minimizes the lower limit of energy per particle among all locally finite planar configurations of centered-disk density one, for every nonnegative completely monotone potential of squared distance, with infinite energies allowed in the comparison. This is the two-dimensional case of the Cohn–Kumar universal optimality conjecture. The manuscripts also claim triangular minimality for unit-background renormalized Riesz energies with 0 < ''s'' < 2 and for the planar Coulomb renormalized energy (the Sandier–Serfaty conjecture), the two-dimensional Brauchart–Hardin–Saff conjecture on the linear term of optimal logarithmic energy on the sphere, and sharpness of the Cohn–Elkies bound for planar circle packing (summary in the collection's contents list).
* '''Sources''' (openai/math repository, commit <code>adc7f12</code>):
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Universal-optimality-of-the-triangular-lattice-September-23-2026 ''Universal optimality of the triangular lattice''] (23 September 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-atomic-certificate-for-triangular-lattice-universal-optimality-September-26-2026 ''An atomic certificate for triangular-lattice universal optimality''] (26 September 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Triangular-minimality-for-planar-Coulomb-renormalized-energy-September-23-2026 ''Triangular minimality for planar Coulomb renormalized energy''] (23 September 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-sharp-Fourier-certificate-for-planar-circle-packing-September-23-2026 ''A sharp Fourier certificate for planar circle packing''] (23 September 2026).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/090.md lean/docs/090.md] states that the Lean formalization proves the universal energy minimality statement above, constructs the sharp Gaussian Fourier minorants with the atomic interpolation construction, and constructs the sharp radial certificate for planar circle packing; the uniqueness statement for periodic equality cases is outside the formalized theorem. The Riesz, Coulomb and spherical-energy statements are not listed in the scope note. The comparator statements are listed in that note.
* '''Background.''' H. Cohn and A. Kumar, ''Universally optimal distribution of points on spheres'' ([https://arxiv.org/abs/math/0607446 arXiv:math/0607446]), formulated the conjecture; H. Cohn, A. Kumar, S. D. Miller, D. Radchenko and M. Viazovska, ''Universal optimality of the E<sub>8</sub> and Leech lattices and interpolation formulas'' ([https://arxiv.org/abs/1902.05438 arXiv:1902.05438]), proved it in dimensions 8 and 24. The planar question appears as Problem 1.1 ("Prove A<sub>2</sub> is universally optimal") of the AIM workshop problem list [http://aimpl.org/discreteaf/1/ ''Discrete geometry and automorphic forms''].

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-11 || X. Callens, [https://github.com/xaviercallens/triangular-universal-optimality-lean xaviercallens/triangular-universal-optimality-lean] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23285631 10.5281/zenodo.23285631], [https://doi.org/10.5281/zenodo.23293429 10.5281/zenodo.23293429]) || Use (formal corollaries) || Lean corollaries of OpenAI's theorem: optimality for the Riesz ''s''-energy for every ''s'' > 0 and at every density, and universal optimality in the sense of Cohn–Kumar–Miller–Radchenko–Viazovska "using lower energy (liminf), which is a weaker notion". It also shows that this lower-energy optimum is not unique: the lattice with one point removed attains it as well. || The README describes an "open red-team review" that is "Not peer reviewed", and states that the corollaries, audits and controls were produced by Claude agents under Xavier Callens's direction.
|-
| 2026-10-13 || M. Colbrook and contributors, [https://github.com/MColbrook/AIM AIM — Open Applied Problems] (GitHub), [https://github.com/MColbrook/AIM/blob/a153f469ee0ea64e876b2ad97c79d252c19a3e22/problems/087-triangular-universal-optimality.md problem 087] and [https://github.com/MColbrook/AIM/blob/a153f469ee0ea64e876b2ad97c79d252c19a3e22/problems/234-abrikosov-global-crystallization.md problem 234] || Catalogue || The collection records its problems 087 (Gaussian-energy optimality of the triangular lattice among periodic configurations) and 234 (global optimality of the Abrikosov triangular lattice) as solved by these manuscripts. || The status review is described as "an AI statement-level review of a published manuscript, not a fresh independent audit of its complete proof or a Lean kernel replay". The collection is not affiliated with the American Institute of Mathematics.
|}

== Notes ==
* The follow-ups state AI assistance as recorded in the table.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Universal optimality of the triangular lattice - Revision history

Aftermath bot: Catalogue status: Formal Conjectures lists Green's Problem 42 as solved with a link to the repository's Lean proof (checked 16 October 2026)

Aftermath bot: New result page: universal optimality of the triangular lattice (public follow-ups linked); AIM catalogue status on the Mahler and matrix multiplication pages; Main Page link