The cost of generating new results on some of mathematics’ long-standing open problems has dropped dramatically, with OpenAI claiming that its Astra model produced machine-checkable proofs for 10 questions that had remained unresolved for at least a decade.
OpenAI published the research on August 1, using the name Astra for its next major model family. The work spans several areas of advanced mathematics, including group theory, high-dimensional geometry, coding theory, quantum complexity, lattice cryptography and extremal combinatorics.
The research was released as a 249-page collection of manuscripts, accompanied by machine-checkable certificates for each of the 10 results. The problems were not routine mathematical exercises: several had remained open for decades and were regarded as significant questions within their respective fields.
Among the reported breakthroughs are a construction demonstrating the existence of non-sofic groups, a disproof of Connes's rigidity conjecture in the theory of von Neumann algebras, and an improved general upper bound for sphere-packing density in high dimensions. The latter improves upon a bound that had remained in place since 1978.
Three of the problems also came from the extensive collection of unsolved questions associated with mathematician Paul Erdős.
The announcement builds on a result reported in May, when the same model family was said to have disproved the Erdős unit distance conjecture, an 80-year-old problem in discrete geometry that had resisted sustained efforts since 1946. Fields Medalist Tim Gowers said he would have recommended the proof for publication in a leading mathematics journal without hesitation. A group of nine mathematicians, including Gowers and Noga Alon, subsequently published a companion paper presenting the proof in a more accessible form for human mathematicians.
Thomas Bloom, who maintains the Erdős problem catalogue, described the August results as “big news” and said they were even more significant than the earlier unit distance result. OpenAI researcher Noam Brown offered a more cautious assessment: “Sadly, no Millennium Prize Problems (yet).”
Machine Verification Changes the Equation
AI research announcements have frequently faced questions over whether reported achievements can be independently evaluated. Benchmarks can be influenced by training data, demonstrations can be selectively presented, and external researchers may have limited ways to reproduce proprietary results.
Astra's mathematical work takes a different approach because the reported proofs were formalized using Lean, a proof assistant designed to verify mathematical arguments step by step. OpenAI also released the certificate files on GitHub under an open license, allowing researchers to download them and run the verification process themselves.
If an individual step does not logically follow from what came before it, the checker rejects the proof. The process therefore does not depend on trusting the organization that produced the result or on subjective interpretation of the argument.
Traditionally, a major mathematical proof goes through peer review, with human experts potentially spending months examining its reasoning before the wider community accepts the result. Machine verification can dramatically shorten the technical verification stage, allowing the validity of a formalized argument to be checked almost immediately.
That distinction makes the Astra announcement different from a conventional AI benchmark. A machine-verified proof can be independently checked even when the underlying model itself is not publicly available.
Questions Around the $2,000 Figure
There are, however, important limitations to the claims.
The selection of the 10 problems was controlled by OpenAI, meaning the published results may not represent the full range of problems the model attempted. The reported $2,000 figure also relates to the successful results rather than the total cost of all experimentation, making it more accurately a measure of the cost of producing the published results than the complete cost of mathematical discovery.
OpenAI researchers also participated in preparing the papers and formalizing the arguments, while the company maintains that Astra generated the mathematical content. Because Astra itself is not available to external researchers, independent reproduction of the model's discovery process is not currently possible.
AI critic Gary Marcus described the release as impressive but substantially oversold. Some mathematicians have also suggested that further scrutiny could reveal that only a portion of the 10 problems represent genuinely unexpected breakthroughs, while others may prove to have been problems that were technically approachable but had not yet received the necessary attention.
Even with those qualifications, one feature remains significant: the results can be mechanically verified. Whether or not the problem selection was optimized for success, a result accompanied by a formal certificate is fundamentally different from an AI-generated claim that cannot be independently checked.
Why Verification Could Matter Beyond Mathematics
The larger implication may extend well beyond mathematical research.
AI systems can generate large quantities of content and technical output, but organizations often struggle to validate that output at the same scale. Human review may work for a handful of documents or analyses, but it becomes increasingly impractical as AI-generated output grows.
Some industries have already addressed this challenge by building automated verification into their workflows.
Chip design is a prominent example. Formal verification systems can mathematically establish whether a circuit meets its specifications, providing an automated layer of assurance that existed well before generative AI became widely used.
At Computex in May, Cadence said it had expanded its design agent toward full autonomy. The system reportedly runs hundreds of simulations through the company's Jasper formal verification engine, reducing a validation cycle that previously took around five weeks to less than a day. Synopsys offers a similar category of technology through VC Formal, which uses static analysis to verify designs rather than relying solely on individual test cases.
The economics are straightforward: when a machine-generated answer can be checked automatically and inexpensively, mistakes become far easier to detect and correct.
The same principle applies to areas such as cryptography, safety-critical software and hardware verification, where formal proof or automated checking is already part of the development process.
As AI systems become capable of generating increasingly sophisticated output, the ability to verify that output may become more important than the ability to generate it.
The central shift is therefore not simply that AI can produce difficult answers more cheaply. It is that the bottleneck is moving from generating an answer to proving that the answer is correct.
.jpg)
