OpenAI Says Astra Found 10 New Math Results. Here’s What the Evidence Shows

A 249-page manuscript and public Lean certificates make OpenAI’s claims unusually inspectable. They still await the independent review that turns a corporate release into accepted mathematics.

On August 1, OpenAI released an unusually inspectable package of mathematical claims: a 249-page manuscript covering ten results in pure mathematics and theoretical computer science, a second document reconstructing how its internal Astra model searched for the arguments, and a public repository of machine-checkable proofs written in Lean.

If the arguments survive expert scrutiny, several would close questions open for decades. One claims the first general improvement since 1978 to the leading asymptotic upper bound for high-dimensional sphere packing. Another claims the existence of a non-sofic group, answering a question posed by Benjamin Weiss in 2000. A third claims an exponential parallel-repetition theorem for general two-player entangled games. The bundle also includes new bounds for error-correcting codes, permanent complexity and the closest vector problem, along with claimed resolutions in operator algebras, convex geometry, Ramsey theory and extremal graph theory.

The qualification is structural: all ten arrive through one company, one unreleased model and one coordinated manuscript. Lean can verify that a formal term has the type claimed under a specified set of definitions and axioms. It cannot certify that a press-release summary perfectly matches the formal theorem, that the formal definitions capture the field’s intended problem, or that the result’s novelty and historical framing are correct. Those are still jobs for mathematicians.

The evidence supports a narrower first verdict. OpenAI has made ten serious research claims and supplied far more inspectable material than a normal corporate announcement. Independent mathematical validation has only begun.

Evidence at a glance

The ten claims, in plain English

1. A new ceiling for the sphere-packing method

Sphere packing asks how densely equal non-overlapping spheres can fill space. Dimensions eight and 24 have celebrated exact answers, but the high-dimensional problem is largely controlled by upper and lower bounds. Since 1978, the best general upper-bound exponent came from the Kabatiansky–Levenshtein method.

The Astra manuscript attacks the Cohn–Elkies linear-programming framework, a Fourier-analytic method that produces upper bounds on packing density. It claims to determine the method’s exact asymptotic exponential power:

$$\lim_{d\to\infty} LP_d^{1/d}=\sqrt{\frac{e}{2\pi}}.$$

Combined with earlier reductions, the result yields an exponent of approximately 0.6044005, compared with roughly 0.5990558 for the Kabatiansky–Levenshtein bound. Because the density is bounded in the form $2^{-\alpha d+o(d)}$, the larger exponent is the stronger upper bound.

That would be the first improvement to the general exponent since 1978. But it is a ceiling on a bounding technique, not a solution of high-dimensional sphere packing. It supplies no denser arrangement of spheres and does not determine the true asymptotic density. The formal endpoint is public in SpherePacking.lean; historical context comes from Cohn and Elkies and Cohn and Zhao.

2. Stricter limits for binary and spherical codes

The coding result has two branches. Binary codes select strings of zeroes and ones that remain far apart under Hamming distance. Spherical codes select well-separated points on a high-dimensional sphere. In both settings, researchers ask how many codewords can coexist at a prescribed separation.

OpenAI claims a hierarchy of semidefinite bounds that strictly improves the best general asymptotic upper bounds. For binary codes at every fixed relative distance $0<\delta<1/2$, the claimed rate is strictly below the optimized McEliece–Rodemich–Rumsey–Welch exponent. For spherical codes at every fixed $0<s<1$, the hierarchy is claimed to beat the optimized Kabatiansky–Levenshtein exponent.

If correct, these are the first unrestricted general improvements to those asymptotic exponents since the late 1970s. The word “upper” matters: the work restricts how large excellent codes could be. It does not construct better practical codes or furnish a new communications system. Nor should it be reported as a capacity result. The formal statements are grouped in MetricCodes.lean, with the classical binary benchmark in MRRW and a useful modern comparison in Samorodnitsky’s 2024 work.

3. The long-sought non-sofic group

Sofic groups were introduced as a broad class that can be approximated by finite symmetric groups. The class includes every amenable group and every residually finite group, and for a quarter-century no one had produced a group outside it. Weiss’s 2000 question, whether every group is sofic, became a conspicuous existence problem.

The manuscript’s answer is no. Its central construction uses the unit group of the binary Leavitt algebra $L_{\mathbb F_2}(1,2)^\times$ and identifies within it a finitely generated subgroup isomorphic to $EL_9(R)$. The formal endpoint establishes the existence of a finitely presented non-sofic group.

This would close the main existence question, but neighboring claims must remain separate. Non-sofic does not automatically mean non-hyperlinear. It does not, by itself, settle every consequence historically associated with soficity. OpenAI thanks several group theorists for discussions, including Henry Bradford, Nathaniel Chapman, Ilya Dogon and Francesco Fournier-Facio; that is evidence of consultation, not a public independent certification. The formal artifact is NonSoficGroup.lean. For background, see Pestov’s survey of the problem and the more recent conditional construction by Kun and Thom.

4. A counterexample at the edge of Connes rigidity

For a countable group $\Gamma$, the group von Neumann algebra $L(\Gamma)$ packages the group into an operator algebra. A central rigidity question asks how much of $\Gamma$ can be recovered from $L(\Gamma)$. Connes conjectured strong rigidity for certain property-(T) groups, and Sorin Popa later formulated a finite-to-one version.

OpenAI claims a countable family of pairwise nonisomorphic, mutually commensurable, finitely generated ICC property-(T) groups whose group von Neumann algebras are all isomorphic. If correct, this disproves the classical conjecture and the finite-to-one formulation while reaching the natural countability ceiling for finitely generated groups.

The scope deserves care. W*-superrigidity is a collection of results and conjectures under different hypotheses; one counterexample family does not erase the subject. The repository’s main formal endpoint establishes the required pair-level phenomenon, while the manuscript builds the infinite family around it. That distinction is exactly the kind of informal-to-formal bridge specialists should inspect. The public Lean entry point is ConnesRigidity/Main.lean. The historical conjecture appears in Connes’s 1982 problem list, and Popa’s formulation appears in his 2013 problem list.

5. A permanent lower bound that does not prove P ≠ NP

The permanent resembles the determinant but lacks its alternating signs. That small syntactic difference makes it a central hard polynomial in algebraic complexity. Proving strong lower bounds for circuits computing the permanent would illuminate the VP-versus-VNP problem, an algebraic analogue of P versus NP.

OpenAI’s result is meaningful but much narrower than that grand objective. For the exact generic permanent over $\mathbb C$, it claims that sufficiently large division-free circuits require at least

$$\frac{n^2}{144}\bigl(\log_2\log_2 n-3\bigr)$$

gates. It also gives nearly quartic lower bounds for formulas: at least $n^4/(128\log_2 n)$ variable leaves in the division-free case, with related bounds when division is permitted in formulas.

In terms of the $N=n^2$ input variables, the circuit result is the first permanent-specific superlinear lower bound for unrestricted division-free circuits, according to the manuscript. It is not superpolynomial, does not cover unrestricted circuits with division, and does not separate VP from VNP. It also says nothing direct about numerical approximation algorithms. The formal statement is in Permanent.lean, with a machine-readable target in the repository’s Comparator challenge.

6. Exponential repetition for entangled games

Parallel repetition asks what happens when players must win many copies of a game at once. In classical two-player games, repeating a game whose value is below one drives the probability of winning every copy down exponentially. Entangled players can coordinate using quantum states, making the general quantum version much harder.

For any finite two-player, one-round entangled game $G$ with entangled value below one, the Astra manuscript claims an exponential bound of the form

$$\omega^*(G^{\otimes n}) \leq \exp\!\left[-c_{qs}\frac{\varepsilon^{13}}{\varepsilon+\log(|A||B|)}n\right].$$

The players may use joint measurements across all repeated coordinates, the questions may be arbitrarily correlated, and they must win every coordinate. Earlier general work by Henry Yuen obtained polynomial decay, while exponential bounds were known for special classes or modified repetition schemes.

The exponent $\varepsilon^{13}$ is not presented as optimal, and the constant is existential. The theorem concerns finite-dimensional tensor-product strategies; it is not automatically a theorem about commuting-operator strategies, multiparty games or multiround protocols. The formal statement is in QuantumParallelRepetition.lean.

7. Fixed-polynomial hardness for closest vector

The closest vector problem asks for the lattice point nearest a given target. It is fundamental in geometry of numbers and complexity theory, and its worst-case hardness helps organize the landscape around lattice problems. OpenAI claims a deterministic polynomial-time many-one reduction from 3SAT to Euclidean GapCVP with approximation factor $n^{1/400}$, using a full-rank integer basis and integer target.

That would replace the previous unconditional $n^{a/\log\log n}$-type hardness with a fixed polynomial factor. The manuscript derives related factors for coding problems and fixed rational $\ell_p$ norms.

This is a complexity-theoretic asymptotic result, not a practical cryptanalytic break. The construction has enormous quantitative overhead: the manuscript’s parameters allow a lattice dimension on the order of $40N^{401}$ for an input of size $N$. It does not directly attack Learning With Errors, ML-KEM, ML-DSA or deployed lattice systems. It also remains far below the familiar $\sqrt n$ approximation barrier. The formal endpoint is GapCVP.lean; the earlier unconditional benchmark is represented by Dinur, Kindler, Raz and Safra.

8. The sharp Ehrhart volume inequality

Ehrhart-type inequalities connect the volume of a convex body with the lattice points it contains. The claimed theorem concerns a full-dimensional compact convex body $K\subset\mathbb R^n$ whose barycenter is the origin and whose only interior lattice point is the origin. OpenAI claims the sharp bound

$$\operatorname{vol}(K)\leq \frac{(n+1)^n}{n!},$$

attained by a simplex.

The formulation is broad: $K$ need not be symmetric, rational or even a polytope, and lattice points may lie on its boundary. The result would settle the sharp constant proposed in work surrounding Berman and Berndtsson and Nill and Paffenholz.

OpenAI’s announcement says the problem had seen “no progress for over a decade.” That phrasing is too sweeping. Researchers have improved related general quantitative bounds during that period; what remained unresolved was the exact sharp inequality in this form. Equality classification beyond the simplex model is also not claimed as complete. The formal endpoint is EhrhartVolumeInequality.lean.

9. The growth scale of multicolor triangle Ramsey numbers

Let $R_k(3)$ be the smallest number of vertices such that every coloring of the edges of a complete graph with $k$ colors contains a monochromatic triangle. Erdős asked whether $R_k(3)^{1/k}$ stays bounded as the number of colors grows.

OpenAI claims a lower bound

$$R_k(3)\geq \left(\frac{c\,k^{1/3}}{\log k}\right)^k.$$

Combined with the known factorial upper bound, this places the growth at $k^{\Theta(k)}$ and forces the kth root to diverge. If correct, that answers the scale question recorded as Erdős Problem #183.

The theorem is asymptotic and existential. It does not determine the sharp exponent hidden in $\Theta(k)$, the best constant, or exact finite Ramsey numbers. OpenAI’s historical line again needs refinement: there was a stronger exponential lower bound in 2021 work by Conlon and Ferber, though the finite-versus-infinite root question remained open. As of the publication cutoff, the independent Erdős Problems database still marked #183 open. The Lean artifact is MulticolorTriangleRamsey.lean.

10. Two counterexamples in extremal graph theory

The final manuscript section contains two related but distinct claims.

The compactness construction gives a finite nonempty family of connected bipartite cyclic graphs whose joint extremal number is $O(n^{21/16})$, even though every individual member has extremal number $\Omega(n^{4/3})$. This refutes a corrected, cycle-only form of an Erdős–Simonovits compactness conjecture. The qualification is necessary because the unrestricted original statement already has simple counterexamples involving forests.

The degeneracy construction gives a fixed connected bipartite 2-degenerate graph $H$ with $\operatorname{ex}(n,H)\geq c n^{3/2+\varepsilon}$ for some $\varepsilon>0$. That contradicts the predicted exponent for the case $r=2$.

Both are existence results; the examples are large, the epsilon is not optimized, and no classification of extremal exponents follows. The Erdős Problems entries associated with the questions (#180 and #146) still showed “open” at the cutoff. OpenAI formalizes both results in CompactnessAndDegeneracy.lean.

What the Lean repository proves—and what it cannot

The public openai/ten-proofs repository is the strongest part of this release. It pins its environment to Lean 4.32.0 and Mathlib 4.32.0, includes machine-readable Comparator targets for selected claims, and declares only three standard axioms inherited through the environment: propositional extensionality, classical choice and quotient soundness. Its formalization.yaml describes twelve formal endpoints because the coding and graph-theory entries each contain two claims; editorially, OpenAI groups them into ten results.

Kingy.ai downloaded the release at commit 0fd01b1c427a4af86493c983550dba485a0911d8 and reconstructed the pinned toolchain in a clean task-local environment. The repository’s bare lake build command failed immediately because lakefile.toml names a nonexistent ConnesRigidity2 default target. Without modifying the release, we then ran its valid lake build All aggregate. The build compiled at least 8,820 of 9,007 jobs—including deep modules in the Connes-rigidity certificate tree—before the local task runner terminated the long-running process. We therefore do not claim a clean end-to-end build. The partial check still establishes that the pinned environment and most of the published project could be reconstructed locally; it is not evidence that every target compiled.

It is not an independent proof audit. A successful Lean build says that Lean’s kernel accepts the formal terms under the encoded definitions. It does not answer four higher-level questions:

1. Statement fidelity: Is the formal theorem exactly the mathematical claim readers think the prose makes?
2. Definition fidelity: Do the encoded objects and hypotheses match standard usage in the relevant field?
3. Reduction fidelity: When the formal endpoint is narrower than the manuscript’s headline, is the surrounding informal reduction complete?
4. Novelty and significance: Is the result genuinely new, and is its historical comparison accurate?

These are not objections to formal proof. They are the reason formal proof and expert review complement one another. Lean removes a vast class of local logical mistakes. It does not turn definitions, translations and literature judgments into mechanical facts.

The repository itself labels the work “agent-reviewed,” not independently human-reviewed. That is the honest status to preserve.

How Astra reportedly worked

OpenAI describes Astra as an internal research system that combines a frontier reasoning model with long-running search. The model generated candidate approaches, abandoned unproductive branches, checked lemmas and assembled arguments. Human researchers then worked with it to prepare the manuscripts; Astra also translated the results into Lean.

The separate reasoning document is unusually useful, but it must be read correctly. It is not a dump of contemporaneous hidden chain-of-thought. OpenAI says the walkthroughs were reconstructed after the fact from original search traces and final papers. They are closer to an editorial map of discovery than to a lab notebook.

The company estimates that solution search for all ten results consumed about $2,000 in tokens when priced at Sol API rates. That number is easy to misread. It is a marginal inference-price estimate, not the all-in cost of Astra’s training, engineering, evaluation, human collaboration, manuscript production, formalization, compute infrastructure or failed research directions. The economics may still be remarkable; the release does not provide enough information to calculate them.

Reproducibility also stops at the artifact boundary. Outsiders can inspect and rebuild the final Lean repository. They cannot rerun the Astra discovery process because Astra is not a released product and the full search system, prompts, checkpoints and execution environment are not public.

Authorship, credit and responsibility

OpenAI lists Astra as the originating system while describing human collaboration in manuscript preparation. The release also explicitly says OpenAI takes responsibility for the work. That last point matters. Mathematical authorship is not just credit for generating a sequence of ideas; it includes accountability for definitions, citations, errors and corrections.

The Leiden Declaration on AI and Mathematics, endorsed by the International Mathematical Union, argues that people and institutions must remain responsible for AI-assisted mathematical claims. OpenAI’s decision to publish the artifacts and accept responsibility fits part of that norm. Presenting an internal model as the discoverer still creates unresolved questions about how individual human contributions, specialist consultations and machine-generated arguments should be credited.

Formalization does not dissolve the issue. Someone chooses the theorem statement, selects definitions, decides which informal reductions sit outside the kernel and writes the historical narrative. Those editorial decisions carry more weight as model output scales.

What would change the verdict

The next evidence should come from outside OpenAI. For each result, the ideal review path is concrete:

• a specialist confirms that the formal statement matches the field’s intended open problem;
• an independent group rebuilds the repository and audits the key definitions and imported assumptions;
• experts check the informal reductions that connect formal endpoints to headline claims;
• literature reviewers test the novelty and “first since” language;
• errors, if found, are logged publicly and corrected with versioned artifacts;
• conventional peer review or equivalent open expert scrutiny develops around the manuscript.

These checks need not wait for a printed journal. Mathematics often validates important work through seminars, circulated notes and public referee-style commentary long before formal publication. But consultation acknowledgments and same-day social reactions are not substitutes for that process.

The validation burden also varies by result. Kingy.ai’s recent reporting on the dimension-three Jacobian counterexample involved exact determinant and collision checks that independent readers could repeat quickly. Astra’s bundle spans ten specialist literatures and several long reductions. Its public certificates improve the starting position, but a credible field-wide review will take longer. For a different model of human-led machine assistance, see Kingy.ai’s coverage of Terence Tao’s machine-assisted proof work.

Kingy.ai has prepared ten entries for its Mathematics & Science Breakthrough Tracker as provisional, Tier 1 claims: primary evidence is public, Lean formalization is available, AI involvement is direct, and independent expert review is pending. The tracker records preserve OpenAI’s ten-result grouping rather than inflating the count to twelve formal endpoints.

Kingy.ai verdict

OpenAI’s Astra release is not a normal AI demo. The company has exposed a dense manuscript, formal source code and a reconstructed account of discovery. That makes the work falsifiable, inspectable and worth immediate attention. The strongest claims, including non-soficity, Connes rigidity, quantum parallel repetition and the first post-1978 general bound improvements, would be major results if experts confirm them.

But “Lean-checked” and “mathematically accepted” are different statuses. Today’s evidence supports ten serious, formally encoded research claims, not ten settled entries in the mathematical canon. The public repository moves the starting line of scrutiny forward. It does not remove the need for scrutiny.

The next move is an independent audit. Specialists must check whether the formal statements, informal reductions and novelty claims line up. OpenAI has supplied unusually good materials for that work; the mathematical verdict will be decided outside OpenAI.