OpenAI previews Astra after internal model advances on 10 difficult math problems

OpenAI has provided an early look at Astra, an unreleased model family intended to handle complex problems that require sustained effort over extended periods. The company says an internal version of the system contributed to 10 advances in mathematics and theoretical computer science.

In a research update, OpenAI said the problems had seen no progress on their central results for at least 10 years, with some remaining unresolved for considerably longer. The work covered areas including high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, quantum complexity, lattice cryptography and extremal combinatorics.

OpenAI cited several results as examples, including work involving non-sofic groups, a disproof of Connes’s rigidity conjecture, improved bounds for high-dimensional sphere packing and solutions to multiple problems associated with mathematician Paul Erdős. The company estimated that generating the solutions required about $2,000 worth of model usage at Sol API rates.

Formal verification was part of the process

Human researchers used the model’s output to develop formal mathematical manuscripts. Astra then translated each argument into a certificate for Lean, a proof assistant that can mechanically check whether the formalized reasoning is valid. This additional verification step is intended to distinguish machine-generated conjectures or arguments from proofs that can be independently checked by software.

OpenAI described Astra as its “next major model,” but has not announced a release date or final product name. Reporting from The Information has also indicated that the company is developing a model family aimed at long-running workloads, including tasks in which AI agents divide portions of a larger problem among themselves.

The model’s eventual branding and availability remain unsettled. It could reportedly appear as GPT-5.7, GPT-6 or under a different name. OpenAI may also offer a less capable version broadly while restricting access to more powerful variants, similar to safety and access policies used by other AI companies.

The reported mathematical achievements highlight the potential of systems that can combine extended reasoning, collaboration and formal verification. However, OpenAI’s claims concern internal research and should be evaluated more fully once supporting technical details, independently reviewable results and product information become available.