OpenAI announced on August 1, 2026 that an internal version of Astra, its next major model, produced new results for ten problems in mathematics and theoretical computer science that had seen no progress on the main result for at least a decade, and in most cases far longer. The problems span high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography, and extremal combinatorics. OpenAI states that the total tokens needed to find these solutions would cost roughly $2,000 at GPT-5.6 Sol API rates, that humans prepared the arguments into manuscripts using the same model, and that the model then formalized each argument in a Lean certificate. ASAP works from OpenAI's own announcement to separate what was newly solved from what remains human work.

The ten results come from eight distinct areas, not one

The ten results OpenAI published are spread across different subfields, and every one of them concerns a problem whose main result had been static for at least ten years. Listed as OpenAI presents them, they run as follows.

First, high-dimensional sphere packing: new upper bounds on sphere-packing density down to the Cohn-Elkies threshold. Second, binary and spherical codes: exponentially improved bounds on the maximum size of binary codes at any prescribed minimum distance, with analogous results for high-dimensional spherical codes. Third, non-sofic groups: a construction establishing their existence, addressing a central open question in group theory. Fourth, Connes's rigidity conjecture: a disproof of the longstanding claim that certain groups are uniquely determined by their von Neumann algebras.

Fifth, arithmetic circuit complexity: new lower bounds for computing the permanent with arithmetic circuits and formulas, including an arithmetic-formula lower bound of order n⁴/log n. Sixth, quantum parallel repetition: an exponential parallel repetition theorem for general two-player quantum games, extending a foundational principle of classical complexity theory. Seventh, the closest vector problem: polynomial-factor hardness of approximation for a foundational lattice question tied to post-quantum cryptography. Eighth, Ehrhart's volume conjecture: determining, in every dimension, the maximum volume of a convex body whose centroid is its only interior lattice point. Ninth, multicolor Ramsey numbers: a superexponential lower bound for multicolor triangle Ramsey numbers, resolving Erdős problem 183. Tenth, extremal number conjectures: results on the compactness and degeneracy conjectures in extremal graph theory, resolving Erdős problems 146 and 180.

OpenAI spells out where the model's work ended and human work began

OpenAI's August 1, 2026 announcement is explicit that the labor divides into three stages, with the model generating and humans packaging. The mathematical arguments themselves were generated by the internal version of Astra. Humans then prepared those arguments into manuscripts, using the same model as a tool. Afterward, the model formalized each argument in a Lean certificate. OpenAI says it helped prepare the manuscripts and formalize the proofs and that it takes responsibility for their correctness. For each solution, OpenAI is also releasing the model's own narration of its thinking process.

There is a precedent behind this release. In May 2026, OpenAI shared an AI-generated disproof of the Erdős unit-distance conjecture, discovered while evaluating an unreleased model, and says that work has already inspired further developments. A footnote lists five subsequent papers, including Bloom, Sawin, Schildkraut and Zhelezov showing the sum-product conjecture is false for real numbers. OpenAI also frames the release against an access initiative it recently announced, ChatGPT for Academic Researchers, which provides 100,000 scientists and mathematicians with free access to its best ChatGPT models.

The $2,000 figure needs to be read for what it measures

The $2,000 number is the figure most likely to travel, so it is worth being precise about its scope. OpenAI's wording covers the tokens needed to find solutions to these problems, converted to Sol API rates. That is the cost of successful search. The human hours spent turning arguments into manuscripts, the additional compute consumed during Lean formalization, and the cost of attempts that did not produce a publishable result are not stated as included.

Underrating the figure would be equally wrong. GPT-5.6 Sol is priced at $5 per million input tokens and $30 per million output tokens as of July 30, 2026, so $2,000 corresponds to compute on the order of tens of millions of tokens. Search that resolved ten problems stalled for a decade or more finished inside a compute budget smaller than one researcher's annual cloud allocation. What matters is not that the absolute number is small but that the unit changed. When the bottleneck on hard problems shifts from compute budget to problem selection and verification, the value of knowing which question to ask goes up rather than down.

One further caveat belongs with the number. The results came from an internal version of Astra, while the conversion uses the published rates for Sol, a model already on sale. Nothing in the announcement states what Astra will cost or how it will be served when it ships. The $2,000 is best read as an order-of-magnitude conversion, not as a reproduction cost.

Lean certificates do not remove the verification burden, they relocate it

Verification is the sharpest friction point for AI-generated mathematics, and it is the constraint the ten Lean certificates in this August 2026 release are aimed at. Long arguments that look plausible but bend somewhere in the middle had to be walked line by line by humans, and that burden meant the volume of claims outran the community's capacity to check them. Formalization attacks exactly this point. When a formal proof compiles, the fact that each step follows within a stated axiomatic system is guaranteed mechanically, and no human recomputation is required.

What formalization guarantees, however, is narrow and specific. Lean confirms that statement B follows from statement A. It does not confirm that A and B faithfully transcribe the problem mathematicians were actually asking. Whether the formal theorem statement is a correct rendering of the original conjecture, whether the definitions are standard, and whether a hypothesis quietly got stronger all still require a human reader. Verification labor did not disappear; it compressed from the whole argument into the much shorter span of statements and definitions.

That is why the structure of this release matters more than any single result. Publishing bare claims makes a community spend its time on adjudication, whereas publishing certificates moves the argument straight from is it correct to what does it mean. OpenAI's request that the mathematical community engage with the results and place them in context reads as a request that presumes exactly this structure.

A company narrowing its own authorship claim is an unusual move

OpenAI states its attribution principle directly: claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system's contribution and the nature of genuine human intellectual work. The company says it helped prepare the manuscripts and formalize the proofs in Lean and takes responsibility for correctness, while the mathematical arguments themselves were generated by its system. It also expresses respect for those concerned about AI's impact on mathematics, including signers of the Leiden declaration on AI and Mathematics.

The direction of the move is what makes it notable. The common corporate reflex is to downplay a system's role to avoid controversy; here the proposal runs the other way, restricting when humans may claim authorship. Applied in practice, the friction lands on academia rather than on the company. Author lists are the unit of hiring, promotion, and grant review, and journals have generally settled on policies that decline to recognize AI systems as authors. If the generator of an argument cannot be listed and humans should not claim it, where these results sit inside existing review structures is an open question.

The way the Leiden declaration is invoked is also worth noting. OpenAI states its position while treating the opposing view as something to respect rather than rebut, conducting the results announcement and the norms discussion in the same document. How mathematics receives this work will depend on that negotiation as much as on whether the proofs hold.

What research groups and companies should adjust now

The immediate practical change is in how research effort is allocated. When deciding how much human time to spend on a long-stalled problem, spending a few days of frontier-model compute first now falls inside a reasonable budget, not because success is expected but because failure costs only compute while success carries a large priority advantage. The presence of the closest vector problem on this list is a specific signal for security organizations preparing post-quantum migrations, since lattice hardness results bear directly on the security arguments underpinning standardization.

On the corporate side, verification infrastructure becomes a real differentiator. Two organizations running the same model will convert its output into trustworthy deliverables at very different speeds depending on whether they can check generated arguments and designs with formal tools. Proof assistants like Lean are not confined to mathematics; they are used for algorithm and protocol correctness as well. A model adoption budget that funds generation and leaves verification empty is misaligned with the division of labor this release demonstrates.

What remains unanswered

The first gap is the success rate. OpenAI describes the ten results as a selection and does not say how many problems were attempted. Selected successes cannot establish how generally the capability transfers to an arbitrary open problem, and the meaning of the $2,000 figure is not settled until that denominator is known.

The second is independent review. Even with Lean certificates attached, whether the formal statements faithfully render the original conjectures and how significant each result is within its field are judgments for the respective communities. OpenAI itself asks the mathematical community to engage deeply and place the results in context. What exists so far is an announcement and supporting material; field-level assessment is still ahead.

The third is Astra itself. The results came from an internal version of a model that has not shipped, and the announcement gives no specifications, release date, or access terms. Until outside researchers know when and on what terms they can use the same capability, this stands as a record of what the tools can reach rather than evidence that the tools have spread.

Source: ASAP analysis based on OpenAI's official announcement "Ten advances in mathematics and theoretical computer science" (August 1, 2026) and the OpenAI API pricing page