- OpenAI says an internal version of its forthcoming Astra model generated ten results spanning sphere packing, coding, group theory, operator algebras, circuit complexity, quantum games, lattices and extremal combinatorics.
[1] - The supporting release includes a 249-page anthology, separate reasoning walkthroughs and Lean 4 formalizations of the principal results.
[2][3] - OpenAI’s formalization manifest reports no unfinished
sorrygoals and lists only standard Lean axioms, but labels the review status “agent-reviewed.” [3] - The closest-vector result strengthens worst-case hardness evidence relevant to lattice cryptography; it does not provide an attack on deployed post-quantum systems.
[2] OpenAI on Saturday published ten claimed advances on longstanding problems in mathematics and theoretical computer science, saying an internal version of its next major model, Astra, generated the mathematical arguments. The most consequential claims include an explicit non-sofic group, a counterexample to Connes’s rigidity conjecture and an exponential parallel-repetition theorem for every finite two-player entangled game.[1][2]
The company released more supporting material than a conventional product announcement: a 249-page manuscript, a 62-page account of the model’s discovery paths and Lean 4 formalizations for the principal results. OpenAI estimates that the model inference used to find the solutions would have cost roughly $2,000 at Sol API rates. Humans then prepared the manuscripts with the model and helped turn the arguments into formal code.[1][2]
The package is not equivalent to completed peer review. OpenAI’s formalization manifest describes the code as “agent-reviewed,” although acknowledgments show that outside specialists commented on the non-sofic-group manuscript and carefully read the Connes-rigidity chapter. Those contributions are meaningful prepublication scrutiny, but the collection does not report formal journal or conference acceptance.[2][3]
The ten claims and what they would establish #
The first chapter determines the claimed asymptotic strength of the Cohn–Elkies linear program for high-dimensional sphere packing. It improves the general packing exponent from about 0.5991 to 0.6044 — described in the manuscript as the first such improvement since 1978 — while also showing that the Cohn–Elkies method cannot surpass the new exponent. The second chapter claims exponential improvements over classical fixed-distance upper bounds for binary and spherical codes across the permitted parameter ranges.[2]
The third chapter constructs an explicit, finitely presented non-sofic group using property-(T) expanders and the binary Leavitt algebra. If accepted, it resolves whether every countable group admits finite permutation approximations. The authors thank Henry Bradford, Michael Chapman, Alon Dogon and Francesco Fournier-Facio for comments, but the acknowledgments do not characterize those comments as endorsements of the final proof.[2]
The fourth chapter constructs infinitely many pairwise nonisomorphic property-(T) groups with isomorphic group von Neumann algebras, contradicting Connes’s rigidity conjecture and answering a related finite-to-one question from Sorin Popa. OpenAI says Popa commented on the historical context and François Charles and Cyril Houdayer carefully read the manuscript. It also reports independent, concurrent work by Shuoxing Zhou reaching a counterexample to the conjecture with assistance from GPT-5.6 Sol, providing separate support for the headline conclusion but not verification of OpenAI’s particular construction.[2]
The fifth chapter proves lower bounds for exact symbolic computation of the permanent over the complex numbers: Ω(n² log log n) gates for unrestricted-reuse, division-free arithmetic circuits and Ω(n⁴/log n) variable-labeled leaves for formulas, even when valid division is allowed. The result advances lower bounds within those models but does not rule out polynomial-size general arithmetic circuits or resolve VP versus VNP, the algebraic analogue of P versus NP.[2]
The sixth chapter claims exponential parallel repetition for every finite two-player entangled game. Earlier general work established polynomial decay, while exponential theorems were available for special or transformed games. The proposed result says that requiring players to win every copy of a repeated game reduces their optimal entangled winning probability exponentially, a soundness-amplification property relevant to quantum complexity and interactive proofs.[2][5]
The seventh chapter gives a deterministic reduction from 3SAT showing that Euclidean closest vector is NP-hard to approximate within n^(1/400). It also claims n^(1/200) hardness for binary nearest-codeword and syndrome-decoding problems and n^(1/(200p)) hardness for closest vector in any fixed rational ℓp norm. The eighth chapter proves Ehrhart’s proposed sharp volume bound, (n+1)^n/n!, in every dimension for a convex body whose barycenter is its sole interior lattice point.[2]
The ninth chapter claims a superexponential lower bound for multicolor triangle Ramsey numbers, establishing Rk(3)=k^Θ(k) and resolving Erdős problem 183. The final chapter gives separate bipartite graph constructions that disprove the Erdős–Simonovits compactness conjecture and an Erdős conjecture about extremal numbers of degenerate bipartite graphs, resolving Erdős problems 146 and 180.[2]
What the Lean certificates establish #
OpenAI’s repository contains separate Lean files corresponding to all ten chapters. Its manifest reports zero sorry placeholders in the main results and lists only propext, Classical.choice and Quot.sound as axioms. The project can be built with Lean 4.32.0 and Mathlib, and the repository includes Comparator configurations intended to permit checking exported proofs with another kernel.[3]
A successful kernel check establishes that the encoded conclusion follows from the encoded definitions and assumptions. It does not by itself determine whether the formal statement faithfully captures the historical conjecture, whether a definition unintentionally weakens the problem or whether the manuscript accurately describes the theorem’s significance. Those are mathematical-review questions rather than type-checking questions.
That distinction is not hypothetical. An independent 2026 case study of a different Lean project found that a development could compile without unfinished goals while still raising serious concerns about definitions, theorem generality and suitability as a reusable mathematical contribution. OpenAI’s extensive certificates materially reduce the risk of an ordinary logical gap, but they do not remove the need for specialist review of the formalization boundary.[4]
No immediate cryptographic break #
The closest-vector and quantum-parallel-repetition chapters have the clearest cryptographic connections. CVP belongs to the family of lattice problems central to modern cryptography, while parallel repetition is used to analyze soundness amplification in proof systems and cryptographic protocols. Neither chapter announces a faster lattice attack, a broken encryption scheme or a practical method for defeating standardized post-quantum cryptography.[2]
The CVP theorem is a worst-case NP-hardness result for a polynomial approximation factor. Deployed lattice cryptography more commonly rests on specific assumptions involving Learning With Errors, shortest-vector problems and average-case-to-worst-case reductions at defined parameter ranges. The new theorem may improve the theoretical map around those assumptions, but translating it into concrete security guarantees would require separate reductions and parameter analysis.
The materials are now public enough for that scrutiny to begin. The outstanding work is to reproduce the builds, compare each Lean declaration with the corresponding open problem and obtain field-specific verdicts on ten arguments that span largely separate research communities.
Companies mentioned #
Further sources #
[[1] OpenAI, “Ten advances in mathematics and theoretical computer science,” August … ↗](https://openai.com/index/ten-advances-in-mathematics/)
[[2] OpenAI, “Ten Advances in Mathematics and Theoretical Computer Science,” 249-pag… ↗](https://cdn.openai.com/pdf/ten-proofs-oai.pdf)
[[3] OpenAI, ten-proofs GitHub repository and formalization manifest. The repository… ↗](https://github.com/openai/ten-proofs)
[[4] Jireh Loreaux et al., “Sorries Are Not the Hard Part: An Expert-Review Case Stu… ↗](https://openreview.net/forum?id=neKROJdC8F)
[[5] Henry Yuen, “A Parallel Repetition Theorem for All Entangled Games,” ICALP 2016… ↗](https://arxiv.org/abs/1604.04340)
[[6] OpenAI, “How the Ideas Came Together: Mathematical Discovery Notes,” August 202… ↗](https://cdn.openai.com/pdf/reasoning-walkthroughs.pdf)
The stories that matter, in one email. Free — unsubscribe anytime.