The limit of a powerful sphere-packing method
How much empty space is unavoidable when equal balls fill a high-dimensional world?
This is not a solution to sphere packing. It determines the asymptotic limit of one of the field’s strongest proof methods in high dimensions. 1manuscript
A concrete starting point
A sphere packing places congruent balls without overlap. The same distance constraint makes sense in any dimension, even when the geometry can no longer be drawn.
The target is density: the fraction of space covered by the balls. The manuscript does not determine the optimal density. It sharpens a universal upper bound and identifies the exact asymptotic limit of the method producing that bound.
A packing is one arrangement. An upper bound rules out every arrangement. The work studies a Fourier-based test that can certify such a universal ceiling, then finds the test’s exact high-dimensional limit. 2Cohn
What mathematicians had before
In 1978, Kabatianskii and Levenshtein showed that the maximum density in dimension d is at most roughly 2−0.59905576d, ignoring smaller-order terms. That was the general asymptotic exponent to beat. 3Kabatianskii
Gorbachev, then Cohn and Elkies, developed another route. Choose a smooth function f that is nonpositive beyond the no-overlap distance, while its Fourier transform is nonnegative everywhere. Summing f over pairs of ball centers gives the same quantity two ways: geometry pushes it down; Fourier analysis pushes it up. The squeeze yields a density ceiling for every packing. 2Cohn
Cohn and Zhao later showed this Fourier linear program was at least as strong as the classical spherical-code route. But its best possible high-dimensional exponent was still unknown. 4Cohn A 2020 paper predicted the answer using ideas connected to the modular bootstrap: the per-dimension root should approach √(e/(2π)). 5Afkhami-Jeddi
Technical layer · the Fourier certificate
Scale the balls to radius ½, so distinct centers are at least 1 apart. Require f(x) ≤ 0 whenever |x| ≥ 1 and require the Fourier transform f̂ to be nonnegative. Poisson summation converts the sum of f over center differences into a frequency-space sum. Comparing signs gives
Δd ≤ (vd / 2d) · f(0) / f̂(0),
where vd is the volume of a unit ball. Optimizing over every admissible f defines LPd. The true density Δd is at most LPd, but they need not be equal. 1manuscript
Astra’s move: stop forgetting where the negative part lives
A natural earlier attack compressed the relevant wave into a global norm—a single score for its total size. It could reach a radius around √(d/(2π)), but not the needed √d/π. The walkthrough gives the diagnosis: the score knew how much negative mass existed, but forgot where it was. 6walkthrough
The new route balances a candidate function against its Fourier transform. After rescaling, their difference becomes an anti-self-Fourier wave: Fourier transformation flips its sign. Its signed total is zero, so half its absolute mass is negative; the packing sign rules force that entire negative half inside one ball of radius R. 6walkthrough
Now location is the whole game. Passing to log-radius and taking a Mellin transform turns radial Fourier transformation into a reflection across a complex strip with a known gamma-function phase. A maximum principle and harmonic measure show that a ball of radius c√d contains exponentially little mass whenever c < 1/π. Such a ball cannot hold the required negative half. Therefore R must be at least (1/π − o(1))√d. 6walkthrough
Replace one particular arrangement of balls with a smooth test function that can judge every packing at once.
At d = 500, the new asymptotic ceiling is about 6.4× tighter.
Read “ceiling,” not “packing.” Neither bar constructs balls that fill space this densely.
The proof map
- Encode all packings. The Cohn–Elkies sign conditions turn pair-counting into one function ratio. 2Cohn
- Balance and subtract. Convert that ratio into the last sign-change radius of a Fourier eigenfunction. 6walkthrough
- Prove the obstruction. Mellin localization shows no admissible wave can change sign before √d/π, at leading order. 6walkthrough
- Construct a match. Deform a Gaussian in Mellin space. A tiny “remote shell” restores decay at large radii without moving the main threshold. 6walkthrough
The last move matters. A lower barrier alone would only say the method cannot perform better. The constructed auxiliary functions approach the same barrier from the other side, proving that the constant is exact for this linear program. 1manuscript
Technical layer · the origin of 1/π
On an interior line of the Mellin strip, the harmonic measure approaches the logistic density p(u) = (π/4) sech²(πu/2). Its logarithmic potential can be evaluated exactly. After integrating, the leading term becomes log(π²c²), which is negative precisely for c < 1/π. That sign creates the exponential local-mass exclusion. 6walkthrough
For the matching side, an ideal deformation shifts the Gaussian saddle by −½ log(π/2), a Wallis-product identity. Truncation makes it usable near the target; a much smaller positive component on a distant interval repairs the far tail. Contour residues handle the remaining small-radius region. 6walkthrough
What was proved—and what was not
The exact theorem is
limd→∞ LPd1/d = √(e/(2π)).
Equivalently, LPd = 2−(0.604400544… + o(1))d. Since the true packing density Δd is at most LPd, this gives a stronger universal upper bound than the 1978 exponent. 1manuscript It also proves that both linked Fourier sign-uncertainty radii are (1/π + o(1))√d. 7manuscript
The theorem does not identify an optimal packing in arbitrary dimension, close the gap between known constructions and upper bounds, or optimize every fixed finite dimension. The equality is about the leading exponential strength of the Cohn–Elkies method as d tends to infinity. 1manuscript
Is the claim overhyped?
The mathematical claim is genuinely substantial at its stated scale. The phrase “sphere packing solved” would be false; “the exact asymptotic power of the Cohn–Elkies bound was determined” is accurate.
“This improves the general high-dimensional exponent for the first time since 1978.”
The manuscript proves 0.604400544… in place of 0.59905576…. Its assertion that this is the first general exponent improvement since 1978 still warrants an independent literature review. 1manuscript
“The leading exponential power of the Cohn–Elkies program is now exact.”
Yes. A universal obstruction and a matching family of admissible functions meet at √(e/(2π)). The accompanying Lean development states the same root limit and certifies the displayed decimal interval. 8formal artifact
“Astra solved high-dimensional sphere packing.”
No. It sharpened an upper bound and characterized one proof framework. It did not determine the true maximum density or construct packings meeting this ceiling. 1manuscript
“The result has been formally and independently validated.”
A large Lean certificate is public, but the repository labels its review status “agent-reviewed.” That is stronger evidence than an unchecked draft, yet it is not the same as independent expert review or journal acceptance. 9formal artifact OpenAI’s announcement is evidence about who reports producing the work, not a substitute for validation. 10announcement
Full bibliography
10 fully annotated sources
- 01 · primary manuscript
OpenAI. Exponential Growth Rate of the Cohn–Elkies Sphere Packing Linear Program — Chapter 1, p. 2, Theorem 1.1 and equations (3)–(4) (PDF p. 4). States the exact root limit and the resulting upper bound on packing density. ↩
- 02 · peer-reviewed predecessor
Henry Cohn and Noam Elkies. New upper bounds on sphere packings I — Annals of Mathematics 157 (2003), Theorem 3.2, pp. 701–702. The Fourier auxiliary-function bound that the new work analyzes. ↩
- 03 · peer-reviewed predecessor
G. A. Kabatianskii and V. I. Levenshtein. On bounds for packings on a sphere and in space — Problems of Information Transmission 14 (1978), Theorem 4, pp. 1–17. Source of the classical high-dimensional exponent used as the comparison point. ↩
- 04 · peer-reviewed predecessor
Henry Cohn and Yufei Zhao. Sphere packing bounds via spherical codes — Duke Mathematical Journal 163 (2014), Theorem 3.4 and the discussion following it. Connects spherical-code bounds to the Cohn–Elkies linear program. ↩
- 05 · peer-reviewed predecessor
N. Afkhami-Jeddi, H. Cohn, T. Hartman, D. de Laat, and A. Tajdini. High-dimensional sphere packing and the modular bootstrap — JHEP 12 (2020), §3, Conjectures 3.1–3.2 and equation (3.3). Conjectures the high-dimensional rate later claimed by the Astra manuscript. ↩
- 06 · reasoning walkthrough
OpenAI. High-Dimensional Sphere Packing and the Euclidean Linear Program — Chapter 1, §§1.1–1.9, PDF pp. 6–10. Explains the failed global-norm route, Mellin localization, harmonic-measure barrier, and matching construction. ↩
- 07 · primary manuscript
OpenAI. Exponential Growth Rate of the Cohn–Elkies Sphere Packing Linear Program — Chapter 1, p. 3, Theorem 1.2 and proof overview (PDF p. 5). States the matching asymptotics for the positive- and negative-Fourier sign radii. ↩
- 08 · formal certificate
OpenAI. SpherePacking.lean — theorems CohnElkies.sharpCohnElkiesManuscriptConclusions and PackingBounds.sharpFullCohnElkiesManuscriptConclusions. Lean statements include the root limit, base-two exponent, decimal interval, and the unrestricted-to-radial bridge. ↩
- 09 · formal certificate
OpenAI. Formalization metadata — review.status and project.status.main_results, entry “Sharp Cohn–Elkies sphere-packing bounds”. The repository describes its review status as “agent-reviewed,” which is evidence about validation scope rather than mathematical novelty. ↩
- 10 · official announcement
OpenAI. Ten advances in mathematics — release overview and research-process description. Used only for attribution and process claims, not as evidence that the theorem is correct. ↩