VibeMathedMath problems solved with AI
Sign in

Sharpness of the Cohn-Elkies linear programming bound in dimension two

Cohn and Elkies (2003) bounded sphere-packing density in Rn\mathbb R^n by any admissible radial ff with f(0)=f^(0)>0f(0)=\widehat f(0)>0, f^≥0\widehat f\ge0 and f(x)≤0f(x)\le0 for ∣x∣≥r|x|\ge r, giving density at most vol(B(0,r/2))\mathrm{vol}(B(0,r/2)). Numerically the bound appeared to match the best packings in dimensions 2, 8 and 24, and their Conjecture 7.3 asserts that in these dimensions an auxiliary function exists attaining the optimal density exactly. Viazovska (dimension 8) and Cohn-Kumar-Miller-Radchenko-Viazovska (dimension 24) constructed such functions; in the plane the optimal density π/(23)\pi/(2\sqrt3) is classical (Thue), but no sharp auxiliary function was known. Does an admissible function exist that makes the Cohn-Elkies bound equal to π/(23)\pi/(2\sqrt3) in dimension two?

Result
Proved(see note)
Status
Candidate (review pending)
AI contribution
AI-discovered
Method
Construction
Field
Discrete geometry; linear programming bounds for packings
Posed by
Henry Cohn and Noam Elkies (Conjecture 7.3, Annals of Mathematics, 2003)
Year posed
2003
Years open
23y
Solved
2026-09-23
Model
Unreleased internal OpenAI model
Vendor
OpenAI
Collaborators
—
Verification
Lean-checked, statement unaudited
Publication
Announced
Collection
OpenAI math release (October 2026), version adc7f12
Significance
30 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Theorem 1.1 constructs a real radial Schwartz function on R2\mathbb R^2 with f^(0)=1\widehat f(0)=1, f(0)=2/3f(0)=2/\sqrt3, f^≥0\widehat f\ge0 and f≤0f\le0 outside the unit disk, so the Cohn-Elkies bound equals the triangular packing density π/(23)\pi/(2\sqrt3). Its zeros beyond radius one lie at integral squared radii, which recovers uniqueness of the triangular packing among periodic equality cases. It does not satisfy the stronger zero-set condition of Cohn-Elkies Conjecture 8.1, and it gives no new packing bound (the planar density was already known).

What the AI did

The release README says every result in openai/math was produced by an unreleased internal OpenAI model with a fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result. This result is not one of the README's two exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region). The manuscript is authored 'OpenAI' and names no human author. The certificate is a radial Schwartz function whose global sign conditions are proved with rigorous interval arithmetic (python-flint) and analytic estimates; the manuscript's README gives the verifier command.

Verification

No independent mathematician has checked this yet. Checked here: Theorem 1.1 of the manuscript was read against Cohn-Elkies Conjecture 7.3 in dimension two; it gives a real radial Schwartz ff with f^(0)=1\widehat f(0)=1, f(0)=2/3f(0)=2/\sqrt3, f^≥0\widehat f\ge0 and f(x)≤0f(x)\le0 for ∣x∣≥1|x|\ge1, which rescales to the requested witness. The manuscript notes that its witness does not meet the extra zero-set requirement of Cohn-Elkies Conjecture 8.1. Lean: lean/ComparatorChallenges/PlanarPacking.json exists with solution_module OAI.Analysis.PlanarPacking.Main, whose file exists at the pinned commit; this challenge is not in lean/formalization.yaml. The statement PlanarPacking.lean was read here: there exists a Schwartz map on the Euclidean plane, radial, with Fourier transform (kernel e−2πi⟨x,ξ⟩e^{-2\pi i\langle x,\xi\rangle}) equal to 1 at 0, value 2/32/\sqrt3 at 0, Fourier transform real and nonnegative everywhere, and f(x)≤0f(x)\le0 for ∥x∥≥1\|x\|\ge1. This states the headline. Not rebuilt here. Permitted axioms: propext, Quot.sound, Classical.choice.

Sources

Changelog1 change

Discussion