More messages, kept safely apart
How many messages can coexist while remaining distinguishable after noise?
Error-correcting codes ask a deceptively simple question: how many messages can we keep far enough apart that noise does not make one look like another? The new manuscript claims the first strict improvement since 1977 and 1978 to two benchmark high-dimensional exponents—one for binary strings, one for points on a sphere.1manuscript That is a serious claim, but it is narrower than “coding theory is solved.”
A concrete starting point
Consider an eight-bit signal. If two valid signals differ in only one position, a single flipped bit can confuse them. If every pair differs in five positions, the messages are easier to distinguish. A binary code is a collection of such bit strings; its distance is the number of positions that differ.1manuscript
Now replace switch patterns with arrows starting at the center of a sphere. Two arrows that nearly overlap are easy to confuse. Two arrows with a wide angle between them are safer. A spherical code is a collection of arrows forced to stay apart. Both problems seek many messages subject to a separation constraint.1manuscript
The new construction replaces one stabilizer-fixed vector per code point with a high-dimensional subspace that moves equivariantly with that point. The trace of two projection operators measures subspace overlap, preserving the positivity needed by the classical counting method while retaining exponentially more representation-theoretic information.1manuscript2walkthrough
How many bits separate the codewords?
Select any bit in the first word. A rust mark identifies a position that differs from the reference word.
What angular separation is required?
For unit vectors, the inner product is the cosine of the angle. A smaller permitted inner product requires a wider angle.
1. Measure separation
A code works only when every pair stays apart: count changed bits, or measure the angle between directions.
What is the problem, exactly?
Let A₂(n,d) be the largest number of length-n binary words whose pairwise Hamming distance is at least d. Let A(n,s) be the largest number of unit vectors in n dimensions whose pairwise inner products are at most s. For unit vectors, inner product is just the cosine of the angle: s close to 1 allows nearly parallel vectors, while s close to 0 demands an angle near 90 degrees.
The result is not a table of exact answers for small n. It studies the exponent as n grows without limit while the relative binary distance δ = d/n, or spherical threshold s, stays fixed.1manuscript An upper bound is a ceiling: it proves that no code above a certain size can exist. It does not construct a code meeting that ceiling.
Suppose an old ceiling behaves like 20.401n and a new one like 20.397n. The exponent falls by only 0.004, but the ratio is 20.004n, which grows exponentially with dimension. These rounded numbers illustrate the scale near the kissing threshold; the manuscript gives 0.39661 versus the published classical 0.400944… at s = 1/2.1manuscript
What the previous approaches did
Delsarte: turn geometry into an accounting certificate
The classical route writes a carefully chosen polynomial in a basis adapted to the space—Krawtchouk or Hahn polynomials for binary codes, Gegenbauer polynomials for spherical codes. Its coefficients provide a positivity condition, while its values on forbidden pairs have the opposite sign. Summing the polynomial over all pairs then traps the code size from above.1manuscript
MRRW: optimize over the whole cube and over shells
In 1977, McEliece, Rodemich, Rumsey, and Welch developed the landmark binary bounds now abbreviated MRRW.4McEliece The stronger “second MRRW” benchmark does not merely use the whole Boolean cube. It also restricts attention to constant-weight layers—strings containing the same number of ones—and optimizes over those layers. This matters because improving only the simpler first MRRW formula can still lose to an interior choice in the full optimization.4McEliece
Kabatianskii–Levenshtein: harmonics plus a spherical cap
In 1978, Kabatianskii and Levenshtein applied the spectral method to spherical codes and added a cap reduction: first find a sufficiently populated cap, then project it to a smaller sphere with a changed angle threshold.5Kabatianskii The correct benchmark is therefore the cap-optimized exponent, not just the direct whole-sphere formula.1manuscript Later work obtained constant-factor improvements for sphere packing, but a constant factor does not change the high-dimensional exponent addressed here.7Cohn
The exact bottleneck: one fixed vector per harmonic layer
In the familiar spectral construction, each retained harmonic space contributes one stabilizer-fixed, or “zonal,” vector associated with a code point. That line is convenient: it produces a scalar positive kernel. But when the harmonic degree grows with dimension, the surrounding stabilizer representation can itself have exponentially many dimensions. The old certificate kept the line and discarded that multiplicity.1manuscript2walkthrough
The obvious fix—replace the line with a large representation—does not automatically produce a positive scalar kernel. A second tempting shortcut, copying a spherical recurrence onto the Boolean cube, actually gives a false answer: at n = 8 it would bound an existing 128-word even-parity code by 508/7, which is less than 128.2walkthrough The coordinate transitions have to come from genuine orthogonal maps, not analogy.
Astra’s moving-subspace insight
For every code point x, attach a large subspace Ex inside one common ambient representation. A symmetry carrying x to y also carries Ex to Ey. If Px projects onto Ex, then Tr(PxPy) measures the overlap between the two subspaces.1manuscript
This overlap is a scalar two-point quantity, yet it comes from a Gram factorization and remains positive in exactly the sense the linear program needs. The final bound contains a ratio “ambient dimension ÷ subspace dimension.” When the moving subspace has exponential dimension, dividing by its rank subtracts a positive term from the old exponent.1manuscript
That distinction is important. Bachoc and Vallentin also used higher stabilizer harmonics, but with a fixed base point in matrix-valued, three-point semidefinite programs. Here the subspace itself moves with each code point, producing a scalar two-point certificate.6Bachoc
The proof does not win by running a larger numerical optimization. It discovers a richer family of certificates inside the old two-point framework: keep the positive scalar overlap, but recover the exponentially large multiplicity hiding behind the classical fixed line.1manuscript
One fixed line per harmonic layer
The scalar kernel stays positive, but the exponentially large stabilizer multiplicity is discarded.
A subspace moves with every code point
Tr(PxPy) remains a positive scalar overlap while retaining the hidden rank.
The proof map
- Identify the high-multiplicity subspaces. On the cube, primitive Boolean harmonic spaces sit across Fourier levels; on the sphere, harmonics on the directions perpendicular to x sit inside ambient harmonic representations. Their dimensions are exponential when their degrees scale with n.1manuscript
- Make them move correctly. Build the actual orthogonal addition/deletion or coordinate-multiplication maps between neighboring layers. Their transition matrices record how the moving spaces interact.1manuscript
- Convert overlap into a code bound. Gram positivity controls the sum over pairs; the distance condition makes off-diagonal contributions non-positive; trace Cauchy–Schwarz supplies the lower estimate. The result contains the favorable ambient-rank ratio D/dE.1manuscript
- Beat the optimized benchmarks, not their easy versions. The binary proof combines a whole-cube construction with a constant-weight construction to cover endpoint and interior MRRW minimizers. The spherical proof carries the cap optimization through a strict multi-row hierarchy and controls parameter sequences that try to escape to infinity.1manuscript2walkthrough
Technical layer · the equations behind the construction
The asymptotic rates are
R₂(δ) = lim supn→∞ (1/n) log₂ A₂(n,⌈δn⌉), Rsph(s) = lim supn→∞ (1/n) log₂ A(n,s).
A moving-subspace certificate with ambient dimension D, fibre rank dE, permitted threshold s, and transition eigenvalue Λ > s has the schematic finite bound
|C| ≤ ((1 − s)/(Λ − s)) · (D/dE).
The prefactor does not affect the exponential rate; D/dE does. For the binary whole-cube construction, its exponent becomes H₂(a) − H₂(b), rather than the classical boundary case H₂(a) at b = 0. For the spherical one-row construction it becomes Hsph(a) − Hsph(b), rather than Hsph(a).1manuscript
The full binary theorem defines κbin(δ) as the better of the whole-cube and constant-weight variational bounds. The full spherical theorem uses interlacing multi-row representations and then applies the same cap reduction as the classical result.
The exact scope of the result
For every fixed 0 < δ < 1/2, the manuscript proves R₂(δ) ≤ κbin(δ) < M₂(δ), where M₂ is the fully optimized second MRRW exponent.1manuscript This is an asymptotic upper-bound improvement for unrestricted binary codes at every fixed relative distance in that range—not an exact formula for A₂(n,d), not a matching lower bound, and not a new decoder.
For every fixed 0 < s < 1, it proves a strict hierarchy of cap-optimized spherical bounds below BKL(s). At the kissing threshold s = 1/2, a released level-two certificate gives an exponent below 0.39661, compared with the classical 0.400944… value.1manuscript Lower is stronger because these are ceilings.
The manuscript also states that the small-angle limit of the spherical hierarchy recovers the sphere-packing exponent ½log₂(2π/e), about 0.6044 in the convention Δn ≤ 2−(0.6044+o(1))n.1manuscript That consequence connects to proof 1; it does not mean spherical codes or sphere packing are exactly solved in finite dimensions.
Assessment of significance
The headline is proportionate because the improvement is strict across the entire fixed-parameter range in two different geometries, and because it changes the exponential rate rather than only a constant factor. The reusable part may be even more important: moving subspaces expose multiplicity that standard two-point spectral constructions had left unused.
The confidence case is stronger than for an unsupported preprint: OpenAI released a large Lean development plus named Comparator targets for central binary and spherical claims.3formal artifact OpenAI also describes a workflow involving human researchers, Astra, proof formalization, and review.8announcement But those are evidence about verification process, not independent acceptance. The manuscript’s priority and correctness claims still deserve specialist checking against the 1970s literature and close review of the boundary arguments.
Is the claim overhyped?
My calibrated verdict: mathematically major if the manuscript and formal statement match and survive independent review; misleading only when retold as a complete solution to coding theory.
The stated bounds strictly beat optimized MRRW and Kabatianskii–Levenshtein across every fixed parameter.
That is exactly what Theorem 1.1 and the spherical hierarchy claim, and central comparison statements appear among the released Lean/Comparator targets.1manuscript3formal artifact
These are the first improvements since 1977 and 1978.
The manuscript scopes this to the general high-dimensional, fixed-parameter exponential exponents after the classical optimizations. Later finite-dimensional, restricted-family, semidefinite, and constant-factor results are not erased by that wording.1manuscript6Bachoc7Cohn
Astra solved error-correcting codes or found optimal codes.
No. The work improves upper bounds. It neither matches them with constructions nor supplies exact maximum sizes or practical encoders and decoders.1manuscript
The community has already confirmed every theorem and the priority claim.
The released formal artifacts are meaningful evidence, but the official materials are not a substitute for independent specialist review.3formal artifact8announcement
Full bibliography
8 fully annotated sources
- 01 · primary manuscript
OpenAI. Ten Advances in Mathematics and Theoretical Computer Science — Chapter 2, abstract, introduction, and Theorems 1.1–1.2, PDF pp. 29–33. The primary source for the definitions, moving-subspace construction, exact asymptotic bounds, and priority claim. ↩
- 02 · reasoning walkthrough
OpenAI. Reasoning Walkthroughs — Chapter 2, §§2.1–2.8, PDF pp. 11–14. Explains the discarded multiplicity, the failed Boolean recurrence, and why both classical optimizations must be beaten. ↩
- 03 · formal certificate
OpenAI. MetricCodes.lean and Comparator targets — binaryRate_lt_classicalRate, Johnson.binaryRate_lt_mrrw, and HigherHierarchy targets; repository commit e62211d. OpenAI-authored Lean artifacts from the same release. They strengthen auditability, but are not independent mathematical review. ↩
- 04 · peer-reviewed predecessor
R. J. McEliece, E. R. Rodemich, H. Rumsey Jr., and L. R. Welch. New upper bounds on the rate of a code via the Delsarte–MacWilliams inequalities — IEEE Transactions on Information Theory 23(2), 157–166 (1977). The primary predecessor for the optimized binary-code exponent known as MRRW. ↩
- 05 · 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(1), 1–17 (1978), especially Theorem 4. The primary predecessor for the spherical-code bound and its cap optimization. ↩
- 06 · peer-reviewed predecessor
C. Bachoc and F. Vallentin. New upper bounds for kissing numbers from semidefinite programming — Journal of the American Mathematical Society 21 (2008), §3. A useful contrast: matrix-valued three-point semidefinite bounds based at a fixed point. ↩
- 07 · peer-reviewed predecessor
Henry Cohn and Yufei Zhao. Sphere packing bounds via spherical codes — Duke Mathematical Journal 163(10), 1965–2002 (2014), abstract and Theorem 1.2. Shows why later constant-factor sphere-packing gains are distinct from improving the fixed-angle exponential rate. ↩
- 08 · official announcement
OpenAI. Ten advances in mathematics and theoretical computer science — “How the results were developed” and “Verification” sections. Used only for OpenAI’s description of its research and verification process, not as evidence that the theorems are correct. ↩