OpenAI's unreleased 'Astra' model reportedly cracked 10 maths problems that stumped humans for decades
The lab says an internal version of its next big model produced fresh results in geometry, cryptography and group theory, at a compute cost of around $2,000 per problem.
Key points
- OpenAI has revealed an unreleased model called Astra, described as its next major AI system, in a research post published this week.
- An internal version of Astra produced 10 new results in mathematics and theoretical computer science, on problems that had seen no progress for at least a decade.
- OpenAI put the compute cost at roughly $2,000 per problem at its Sol API rates.
- Every proof was formalised as a Lean certificate, meaning a machine-checkable file, so the maths could be verified independently.
- The model may ship as GPT-5.7, GPT-6, or under another name, with no release date confirmed.
OpenAI has pulled the curtain back on Astra, an unreleased AI model it says has already produced ten fresh results in mathematics and theoretical computer science. The company describes Astra as "our next major model" and says the problems it cracked had seen no serious progress in at least ten years, and usually much longer.
This is a research announcement, not a product launch. But it is the sort of announcement that shifts what people expect the next generation of AI to do.
What did Astra actually solve?
Astra worked on long-standing open problems across pure maths and theoretical computer science, the kind that sit unsolved in academic papers for decades. OpenAI lists high-dimensional geometry, coding theory, group theory, quantum complexity, lattice cryptography (the maths behind some future-proof encryption), and extremal combinatorics among the areas.
Specific results include a proof that so-called non-sofic groups exist, a disproof of Connes's rigidity conjecture, new bounds on how densely you can pack spheres in high dimensions, and answers to several questions first posed by the Hungarian mathematician Paul Erdős. If those names mean nothing to you, that is fine. The short version: these are problems mathematicians have been chewing on for a very long time.
Human researchers took the model's arguments and wrote them up as formal manuscripts. Astra then translated each proof into Lean, a mathematical verification system that checks logic step by step. In practice, that means the results are not just "the AI said so". A separate piece of software confirmed the reasoning holds.
OpenAI puts the compute bill at around $2,000 per problem at its Sol API rates. For a decade-old open question in pure maths, that is startlingly cheap.
Will ordinary people ever use this?
Not directly, and not soon. Astra is aimed at long-running workloads where multiple AI agents, meaning software programs that can act on their own, collaborate on different parts of a bigger problem. Think research and engineering pipelines, not chatbots answering emails.
As first reported by BleepingComputer, OpenAI has not decided whether the model launches as GPT-5.7, GPT-6, or under a different name entirely. The company may also follow the pattern Anthropic has used with Claude: release a lighter version to the public and gate the more capable variant behind special approval.
Why does this matter for security?
The cryptography angle is the one worth watching. Astra reportedly worked on lattice cryptography, which is the maths underpinning the post-quantum encryption standards governments and cloud providers are now rolling out. Better AI-assisted proofs cut both ways. They can strengthen the case for a scheme, or find weaknesses in one.
There is no claim here that Astra has broken any real-world cryptography. The failure mode to watch for is subtler: research-grade AI accelerating the discovery of edge cases in schemes that vendors have already shipped. If your organisation has started migrating to post-quantum algorithms in AWS KMS, Azure Key Vault or Google Cloud KMS, keep an eye on the standards bodies over the next year.
One thing the post-mortem will say, if any of this pans out: the gap between "academic curiosity" and "production risk" got shorter again.
Operational takeaway: track your cryptographic inventory now, so when a scheme does get downgraded you know where it lives.
