Riesz-energy, finiteness and every-density corollaries of the openai/math planar universal-optimality theorem, kernel-checked in Lean 4
- 1SocrateAI Lab
Abstract
The openai/math release contains an AI-generated Lean 4 proof that the triangular lattice A of covolume one minimises the lower g-energy among all locally finite planar configurations of density one, for every smooth completely monotone g (theorem universal_energy_minimum; Comparator-accepted by us under the pinned toolchain). Inside that pinned environment we derive and kernel-check three named consequences, using only the axioms propext, Classical.choice and Quot.sound: (D1) for every s > 0 the Riesz potential t ↦ t-s/2 (i.e. |x-y|-s) is admissible, so the triangular lattice minimises the Riesz s-energy among all locally finite density-one configurations; (D1b) for s > 2 the lattice's Riesz s-energy (an Epstein zeta value) is finite, so D1 compares with a finite, attained minimum (for 0 < s ≤ 2 the lattice side is infinite and D1 only says E(C) = ∞); (D2) for every density ρ > 0 and every admissible g, the rescaled lattice ρ-1/2A has density ρ and minimises the g-energy among all locally finite density-ρ configurations; without the rescaling the statement is false (proved in Lean at ρ = 1/4, s = 4). The Riesz form ρs/2 Σ|a|-s ≤ E(C) is also kernel-checked. Mathematically each step is short (complete monotonicity of t-s/2, scaling), and the upstream manuscript already states informally that inverse powers are included; what is new is the kernel-checked form, a statement-fidelity audit against Cohn–Kumar–Miller–Radchenko–Viazovska's lower-energy formulation, planted negative controls, and re-verification by separate instances of the same AI model (producer ≠ verifier). Everything is conditional on the upstream theorem, which has not been peer reviewed and which, by its authors' account, does not claim the stronger per-potential form of the Cohn–Kumar conjecture. The Lean proofs, audit, verification runs and drafting were performed by the AI model Claude (Anthropic) under the author's direction; the author is responsible for the content.
Related
- The triangular lattice minimises the planar Yukawa energy at every density and for every finite mixture of screening lengths: kernel-checked corollaries of planar universal optimality, a human proof, and an exact-potential CVODE consistency study
- Planar universal optimality, tiered: kernel-checked consequences, a non-uniqueness theorem, and a CVODE N-body consistency check for the Yukawa interaction
- The Serre-Grothendieck Finiteness Theorem for the cohomology of coherent sheaves
- Uniqueness of the hexagonal lattice's universal optimality
- Optimality in a Multilinear Extension of Kwapień's Theorem
BibTeX
@misc{callens2026rieszenergy,
title = {{Riesz-energy, finiteness and every-density corollaries of the openai/math planar universal-optimality theorem, kernel-checked in Lean 4}},
author = {Xavier Callens},
howpublished = {Zenodo (CERN European Organization for Nuclear Research)},
year = {2026},
month = oct,
doi = {10.5281/zenodo.23285630},
url = {https://doi.org/10.5281/zenodo.23285630},
note = {CC BY},
}
RIS
TY - UNPB
TI - Riesz-energy, finiteness and every-density corollaries of the openai/math planar universal-optimality theorem, kernel-checked in Lean 4
AU - Xavier Callens
PY - 2026
DA - 2026/10/10
PB - Zenodo (CERN European Organization for Nuclear Research)
DO - 10.5281/zenodo.23285630
UR - https://doi.org/10.5281/zenodo.23285630
AB - The openai/math release contains an AI-generated Lean 4 proof that the triangular lattice A of covolume one minimises the lower g-energy among all locally finite planar configurations of density one, for every smooth completely monotone g (theorem universal_energy_minimum; Comparator-accepted by us under the pinned toolchain). Inside that pinned environment we derive and kernel-check three named consequences, using only the axioms propext, Classical.choice and Quot.sound: (D1) for every s > 0 the Riesz potential t ↦ t-s/2 (i.e. |x-y|-s) is admissible, so the triangular lattice minimises the Riesz s-energy among all locally finite density-one configurations; (D1b) for s > 2 the lattice's Riesz s-energy (an Epstein zeta value) is finite, so D1 compares with a finite, attained minimum (for 0 < s ≤ 2 the lattice side is infinite and D1 only says E(C) = ∞); (D2) for every density ρ > 0 and every admissible g, the rescaled lattice ρ-1/2A has density ρ and minimises the g-energy among all locally finite density-ρ configurations; without the rescaling the statement is false (proved in Lean at ρ = 1/4, s = 4). The Riesz form ρs/2 Σ|a|-s ≤ E(C) is also kernel-checked. Mathematically each step is short (complete monotonicity of t-s/2, scaling), and the upstream manuscript already states informally that inverse powers are included; what is new is the kernel-checked form, a statement-fidelity audit against Cohn–Kumar–Miller–Radchenko–Viazovska's lower-energy formulation, planted negative controls, and re-verification by separate instances of the same AI model (producer ≠ verifier). Everything is conditional on the upstream theorem, which has not been peer reviewed and which, by its authors' account, does not claim the stronger per-potential form of the Cohn–Kumar conjecture. The Lean proofs, audit, verification runs and drafting were performed by the AI model Claude (Anthropic) under the author's direction; the author is responsible for the content.
ER -