OpenAI says its next model solved ten mathematics problems that sat unsolved for as long as three decades, and the work cost roughly $2,000 in compute. No peer review has happened yet, and OpenAI has not said who deserves credit for the results, the model or the researchers who checked its work.
Ten Open Problems, One Small Budget
OpenAI published the results on August 1, under the title “Ten advances in mathematics and theoretical computer science.” The system behind the work, called Astra internally, is what OpenAI describes as its next major model, built to work on problems for hours or days at a stretch using multiple coordinating agents rather than a single pass. CEO Sam Altman has already demonstrated Astra to policymakers in Washington, and OpenAI has not decided whether it ships as GPT-6 or a variant of GPT-5.
The ten problems span group theory, geometry, coding theory, and computational complexity. They include a resolution connected to non-sofic groups, progress on Connes’s rigidity conjecture, new bounds on multicolor Ramsey numbers, and results touching high-dimensional sphere packing and the closest vector problem. Astra generated the underlying mathematical arguments. Researchers, working with the same model, turned those arguments into manuscripts. Every proof was then formalized in Lean, a formal verification language that produces a machine-checked certificate rather than relying on a human reviewer’s judgment call, and OpenAI posted the certificates publicly on GitHub. The company estimates the entire effort cost around $2,000 in API-level compute, less than many corporate dinners.
The Price Tag Matters More Than the Proofs
The cost figure carries more business weight than any individual proof. Decades-old open problems solved for a few thousand dollars point to a shift in the economics of research labor, not just a demonstration of mathematical skill. A university mathematics department spends years and multiple salaries chasing a single open conjecture. Astra’s run suggests that cost structure is no longer fixed, at least for problems that can be checked automatically.
Mathematicians remain split on what the results prove. Thomas Bloom, a mathematician who reviewed the work, called it “big news” while rejecting the idea that AI is replacing mathematicians, since the systems draw on theory that mathematicians built in the first place. Some researchers describe the non-sofic groups result as a genuine, decades-old open question finally resolved. Others point out that mathematics is an unusually favorable domain for AI precisely because every proof can be checked automatically through systems like Lean, a verification loop most real-world business and scientific problems simply do not have.
OpenAI itself has stopped short of claiming the proofs belong to a human author, stating that crediting a person for work a system generated end to end would misrepresent the system’s contribution. Signers of the Leiden Declaration on AI and Mathematics have raised similar concerns about how credit should be assigned. Peer reviewers have not yet completed a review, and authorship credit remains under negotiation.
What This Signals Before the Model Even Ships
My take: the announcement functions as a pre-launch showcase timed ahead of a GPT-6 decision, and mathematics was the friendliest possible venue for it. Verifiable proofs let OpenAI demonstrate extended, multi-agent reasoning without the messier judgment calls that come with open-ended business problems, where there is no Lean certificate to confirm the model got it right.
Companies evaluating agentic AI for research and development should read the math results as a controlled demo, not a preview of how the technology handles ambiguous, real-world work. The unresolved authorship question deserves more attention than the proofs themselves. If OpenAI cannot yet say who owns credit for output its own model produced, procurement and legal teams evaluating agentic AI for internal research face the identical question at a messier scale, without a public relations team to soften it.
Astra’s math results will go through formal peer review over the coming months, and that process, more than the headline number, will show whether the system reasons or simply searches faster than anyone bothered to before. Until verification and authorship catch up with capability, businesses eyeing agentic AI for serious research should treat the demo as impressive housekeeping, not a blueprint.
