OpenAI's next-generation flagship AI model, 'Astra,' has achieved new results in 10 mathematical and theoretical computer science problems, enabling machine verification by formalizing proofs using Lean 4.
On August 1, 2026, OpenAI announced that an internal version of its next-generation flagship AI model, 'Astra,' had made new progress on 10 unsolved problems spanning mathematics and theoretical computer science. The problems in question were 'problems that remained unsolved and for which there had been no progress on major conclusions for at least 10 years,' and OpenAI has released a 249-page paper and data that can be used to mechanically examine the proofs.
Ten advances in mathematics and theoretical computer science | OpenAI
OpenAI now evaluates the mathematical capabilities of its models not only on test questions but also on unsolved research problems. In May 2026, OpenAI reported that an unpublished model had refuted the unit distance conjecture proposed by mathematician Paul Erdős.
OpenAI successfully disproves a mathematical conjecture that had remained unsolved for nearly 80 years, a discovery that even surprised human mathematicians, who say 'AI has gone beyond being just an assistant' - GIGAZINE
This announcement involves using an unpublished model to tackle unresolved problems in multiple fields, and presenting 10 of the results obtained as a result.
According to OpenAI, the mathematical arguments generated by Astra were compiled into a paper manuscript by human staff, and then Astra formalized each argument using 'Lean 4' software, which uses rigorous notation to describe theorems and preconditions and verifies that each stage of the reasoning follows rules. The repository released on GitHub contains 10 Lean-formatted proof data, as well as instructions on how to construct the entire proof and a guide to independent checking tools.
GitHub - openai/ten-proofs: Lean certificates accompanying proofs in mathematics and theoretical computer science · GitHub
https://github.com/openai/ten-proofs
The following are the 10 achievements released by OpenAI.
- Improve the upper limit of high-dimensional sphere packing density to the limit achievable with the Kohn-Elkies method.
- Derive an exponentially stronger upper bound than previously known for the maximum size of binary codes and spherical codes.
- Construct a non-Sophic group that cannot be approximated by finite permutations.
- A counterexample to Connes's rigidity conjecture, which states that a particular group is uniquely determined by the corresponding group, the von Neumann algebra.
- Proving a new lower bound on the computational complexity of arithmetic circuits and arithmetic formulas for calculating the permanents of matrices.
- Proving an exponential parallel iteration theorem for any finite two-player game that utilizes quantum entanglement.
Recently, I proved that approximating vector problems is difficult even when allowing polynomial-multiple errors with respect to the lattice dimension.
- Proving Ehrhardt's volume conjecture in all dimensions for a convex body where only the centroid is an internal lattice point.
- Proving a hyperexponential lower bound for the multicolor triangle Ramsey number.
- Construct counterexamples for both the compactness conjecture and the degeneration conjecture in extreme value graph theory.
The researchers have improved the general upper bounds in higher dimensions for binary codes and spherical codes for the first time since 1977 and 1978, respectively, and also improved the general higher-dimensional exponential for sphere packings for the first time since 1978. In quantum computation theory, they have extended the 'parallel iteration theorem,' which states that the probability of winning all games decreases exponentially when the same game is repeated in parallel, to any finite two-player game that utilizes quantum entanglement.
The total number of tokens needed for the solution search, when applied to the cost of OpenAI's 'Sol API,' comes to approximately $2,000 (approximately 310,000 yen).
OpenAI also publishes explanatory materials (PDF files) in which it has fed the original thought process and completed papers into another AI model to reconstruct the process leading to the proof. The explanatory materials do not simply reproduce the original thought process as is, but rather organize the failed approaches, shifts in perspective, and final ideas into an easy-to-understand explanation.
On the other hand, some articles argue that 'even after the widespread adoption of mathematical AI, humans may not be able to continue studying mathematics in the same way as before.' These articles argue that because mathematics is applied to science and engineering, it is not a closed activity like chess, and that AI may advance mathematics, science, and engineering without human understanding.
OpenAI explicitly states that Astra generated the mathematical arguments themselves, and that it is responsible for the correctness of the proofs, having been involved in drafting the paper and formalizing it using Lean. With 10 proofs released prior to the publication of Astra itself, it is hoped that the mathematical community will now position these results within existing research and use them to drive new research.
Related Posts:
in AI, Posted by log1d_ts