OpenAI claim summary for Math-2316

Linear-Programming Sharpness and Universal Lattice Optimality

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 090; 2026-09-26), the asserted result is that the triangular lattice minimizes the lower per-particle energy for all nonnegative completely monotone squared-distance potentials among centered-density-one planar configurations; In manuscript 2 (family 090; 2026-09-23), the asserted result is that the triangular lattice minimizes that full class of planar pair energies and also the stated logarithmic and Riesz renormalized energies, including corresponding jellium minima.

Mathematical statement of the claimed result

Manuscript 1.

Let $b=\sqrt3/2$ and $A=b^{-1/2}\{m(1,0)+n(1/2,b):m,n\in\mathbb Z\}$, the density-one triangular lattice. A locally finite planar configuration $\mathcal C$ has centered-disk density one if $N_R=|\mathcal C\cap B_R|$ satisfies $N_R/(\pi R^2)\to1$. For smooth $g:(0,\infty)\to[0,\infty)$ with $(-1)^jg^{(j)}(t)\ge0$ for every $j\ge0,t>0$, set \[ E_g(\mathcal C)=\liminf_{R\to\infty}\frac1{N_R} \sum_{\substack{x,y\in\mathcal C\cap B_R\\x\ne y}}g(|x-y|^2). \] The asserted universal comparison is \[ E_g(\mathcal C)\ge E_g(A)=\sum_{a\in A\setminus\{0\}}g(|a|^2). \] Pairs are ordered, and the inequality is interpreted in the extended nonnegative reals; periodicity or uniform local counting bounds are not required.

Manuscript 2.

Let $A=\sqrt{2/\sqrt3}[\mathbb Z(1,0)+\mathbb Z(1/2,\sqrt3/2)]$. A locally finite planar configuration $\mathcal C$ has centered-disk density one when $|\mathcal C\cap B_R|/(\pi R^2)\to1$. For every smooth completely monotone $g:(0,\infty)\to[0,\infty)$, meaning $(-1)^rg^{(r)}\ge0$ for all integers $r\ge0$, define the ordered-pair energy per point \[ E_g(\mathcal C)=\liminf_{R\to\infty}\frac1{|\mathcal C\cap B_R|} \sum_{\substack{x,y\in\mathcal C\cap B_R\\x\ne y}}g(|x-y|^2). \] The claimed universal inequality, including infinite values, is \[ E_g(\mathcal C)\ge\sum_{a\in A\setminus\{0\}}g(|a|^2)=E_g(A). \] Its cited renormalized-energy extension allows $0\le s<2$. Set $g_0(X)=-\log|X|$, $g_s(X)=|X|^{-s}$ for $s>0$, $k=0$ at $s=0$ and $k=1$ otherwise, $w_s=1$ at $s=0$ and $w_s=|y|^{s-1}$ otherwise, and $\kappa_0=2\pi$, $\kappa_s=4\pi$ for $s>0$. Admissible gradient fields obey \[ -\operatorname{div}(w_sE)=\kappa_s(\sum_{p\in\mathcal C}\delta_{(p,0)}-\delta_{\mathbb R^2}) \] in $\mathbb R^{2+k}$, with $w_sE$ locally integrable and $E$ locally in $L^t$ for some $1<t<2$ at $s=0$, or $1<t<\min(2,2/s,3/(s+1))$ at $s>0$. For $f_{\eta}=(g_s-g_s(\eta))_+$ and $E_{\eta}=E-\sum_p\nabla f_{\eta}(\cdot-(p,0))$, use the normalization \[ W_s(\mathcal C)=\inf_E\lim_{\eta\downarrow0}\limsup_{R\to\infty} \left[\frac1{R^2}\int_{[-R/2,R/2]^2\times\mathbb R^k}w_s|E_{\eta}|^2 -\kappa_sg_s(\eta)\right]. \] The periodic version $W_{s,L}$ uses the mean-zero periodic potential and replaces $R^{-2}$ by reciprocal torus area. For every integer $n\ge1$, $N=n^2$, and every $N$ distinct points on $\mathbb R^2/(nA)$, the claim is \[ W_{s,nA}(a_1,\ldots,a_N)\ge W_{s,nA}(A/(nA)),\qquad W_s(\mathcal C)\ge W_s(A),\qquad e_{\rm Jel}^{(s)}=\kappa_s^{-1}W_s(A). \] Here $e_{\rm Jel}^{(s)}$ denotes the thermodynamic minimum per unit area of the ordered-pair $g_s$ interaction with a uniform density-one neutralizing background, including both particle--background and background--background terms.

Outline of the argument

For manuscript 1 (family 090; 2026-09-26), sharp Gaussian minorants are obtained by solving finite atomic interpolation systems and controlling the infinite correction. Fourier positivity transfers each Gaussian bound to general configurations, and positive Laplace mixtures include singular potentials and infinite energies.

For manuscript 2 (family 090; 2026-09-23), cardinal spectral interpolation is certified using positive quadrature and rigorous finite parameter bounds. Sharp Gaussian Fourier comparisons are mixed to treat general potentials, while heat-kernel comparison passes to renormalized and jellium energies.

Formal verification

For manuscript 1 (family 090; 2026-09-26), OpenAI lists Lean statements for this assertion: the triangular lattice minimizes the lower per-particle energy for all nonnegative completely monotone squared-distance potentials among centered-density-one planar configurations.

This coverage does not establish a formal proof of the complete problem as stated here.

No Lean formalization is listed at this snapshot for manuscript 2 (family 090; 2026-09-23).

The linked family Comparator checks are AtomicGaussian.lean, PlanarPacking.lean, TriangularEnergy.lean, TriangularGaussian.lean.

Their named declarations include OAI.AtomicTriangular.sharp_gaussian_minorants_atomic, OAI.AtomicTriangular.sharp_gaussian_minorants_with_construction, OAI.AtomicTriangular.universal_energy_minimum, OAI.sharp_fourier_certificate.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

• OpenAI, An atomic certificate for triangular-lattice universal optimality, 2026-09-26; citation key OAI:An-atomic-certificate-for-triangular-lattice-universal-optimality-September-26-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:universal.
• OpenAI, Universal optimality of the triangular lattice, 2026-09-23; citation key OAI:Universal-optimality-of-the-triangular-lattice-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:universal, eq:main-inequality.
• Family 090: Lean scope.
• Comparator AtomicGaussian.json.
• Comparator AtomicGaussian.lean.
• Comparator PlanarPacking.json.
• Comparator PlanarPacking.lean.
• Comparator TriangularEnergy.json.
• Comparator TriangularEnergy.lean.
• Comparator TriangularGaussian.json.
• Comparator TriangularGaussian.lean.
• OpenAI catalogue entry.