On August 1, 2026, OpenAI published something unusual for an artificial intelligence announcement: a way to prove itself wrong. Ten math problems left unsolved for decades, ten proofs produced by OpenAI Astra, and above all ten files posted on GitHub that anyone can verify on their own machine.
The most talked-about result concerns a question posed in 1999 that went unanswered for twenty-seven years. The most debated figure fits in four characters: $2,000 in compute for the whole set.
Here is what was announced, what is actually verifiable by anyone, and what part of the math community holds against this approach.
OpenAI Astra: What Was Announced on August 1
On August 1, 2026, OpenAI published a report claiming an unusual breakthrough. Its next model, internally named « Astra, » reportedly produced new results on ten open problems in mathematics and theoretical computer science, questions no one had fully answered before. Some of these problems had gone unsolved for ten years, others for nearly thirty, spread across eight distinct fields.
Astra is not available to anyone outside OpenAI. No outside researcher can test it or verify the results independently. The company nonetheless published three documents to back up its announcement: a 249-page technical manuscript, a 62-page narrative detailing the method used, and proof certificates in Lean 4 format (a proof assistant, software that mechanically checks whether a mathematical argument holds) posted on GitHub.
According to OpenAI, these are not partial results. The ten problems were reportedly solved in full, with each proof checked using Lean. Noam Brown, a researcher at OpenAI, tempers the scope of the announcement by noting these are not the Millennium Prize Problems, the seven most famous puzzles in mathematics, each worth a million dollars. Sébastien Bubeck, OpenAI’s head of math research, for his part called the results « beautiful. »
The pace of artificial intelligence announcements picked up again this summer, between leaked rival models and new benchmark records, as shown by this roundup of a particularly packed week for AI. In this climate, some observers wonder whether Astra will become the basis for a future GPT-6. OpenAI has not confirmed any link between the two.
The Ten Problems, and the One That Really Matters
OpenAI Astra didn’t deliver a single result, but ten, spread across fields far removed from one another: group theory, cryptography, combinatorics (the art of counting the ways to combine objects), and geometry. Some tighten bounds that had stood for decades, another flatly disproves a conjecture. Just one of the ten settles a problem left open for twenty-seven years.
| Result | Domain |
|---|---|
| Non-sofic groups | Group theory |
| Sphere packing | High-dimensional geometry |
| Binary and spherical codes | Error-correcting code theory |
| Connes rigidity conjecture | Operator algebras |
| Arithmetic circuit complexity | Permanent computation |
| Quantum parallel repetition | Two-player quantum games |
| Closest vector | Euclidean lattice cryptography |
| Ehrhart volume conjecture | Discrete geometry |
| Multicolor Ramsey numbers | Combinatorics (problem 183 in the Erdős catalog) |
| Extremal numbers | Graph theory (problems 146 and 180 in the Erdős catalog) |
In mathematics, a group is a structure that describes symmetries and transformations, a bit like a catalog of every possible motion of an object. A group is called sofic if it can be mimicked, as closely as you like, by mixtures of a finite number of objects, a kind of simplified, finite copy of the same behavior. Every group mathematicians encounter day to day satisfies this property, including the most studied families in the field.
Mikhail Gromov introduced this notion in 1999. Since then, no one had managed to prove that every group is sofic, nor to exhibit a single one that isn’t. OpenAI Astra builds the first explicit example of a non-sofic group, ending twenty-seven years of uncertainty on the question. This is the result that drew the most attention in the announcement, more than the other nine combined.
Thomas Bloom, who runs the site listing Erdős’s open problems, called these results « big news. » He considers them more significant than the previous AI-found counterexample to the unit distance conjecture.
Tim Gowers, a Fields Medalist, the highest honor in mathematics, had already recommended an AI-produced proof for publication in Annals of Mathematics, one of the field’s most prestigious journals. His endorsement adds weight to a string of results that is starting to intrigue the mathematical community as a whole.
The Real Break: The Proof Is on GitHub, and It Checks Itself
An artificial intelligence announcement usually relies on a score obtained on a test chosen by the lab itself. There’s little way to verify it other than taking the company’s word for it, much like the scores announced when a new model launches. This time, OpenAI changes its approach completely.
Lean is both a programming language and a proof assistant. It forces every step of a mathematical argument to be written out in machine-readable detail. Its software core delivers a binary verdict: either the proof compiles, meaning the code passes verification without error, or it fails. No middle ground, no room for interpretation. Checking these proofs therefore requires no math PhD, no trust in OpenAI, and no months waiting on a review committee.
The repository, the space where a project’s code and files are stored and shared publicly, is located at github.com/openai/ten-proofs. It is released under the Apache 2.0 license, an open license that lets anyone download, use, and redistribute it. It’s a standard Lean 4 project, on version 4.32, built on mathlib, Lean’s community math library, and on Lake, its project manager.
Each result has its own plainly named file: NonSoficGroup.lean, ConnesRigidity.lean, SpherePacking.lean, Permanent.lean, QuantumParallelRepetition.lean, GapCVP.lean, MetricCodes.lean, MulticolorTriangleRamsey.lean, EhrhartVolumeInequality.lean, CompactnessAndDegeneracy.lean. The repository has only a single commit, meaning a single recorded change, and a single contributor. Lean accounts for 100% of the code.
The figure that matters most lies elsewhere. The count of « sorry » is zero. In Lean, « sorry » is the keyword that lets you admit a step without proving it, a way of saying « we’ll get to it later. » Zero « sorry » means no step was left unresolved across the ten proofs.
The README, the presentation file that shows up first on the repository’s page, is titled « Ten Advances in Mathematics and Theoretical Computer Science. » At the time of the screenshot, the project had 477 stars and 46 forks, copies of the repository made by other users to study or reuse it.
$2,000, and This Is Where It Gets Dizzying
The figure OpenAI put forward is worth pausing on. Producing the ten solutions reportedly cost about $2,000 in compute, at the rates of the company’s Sol API. That amount corresponds to the tokens (the unit of text that language models bill for) consumed to generate the published answers, nothing more.
This calculation leaves out the failed attempts. OpenAI doesn’t say how many avenues were explored before arriving at the ten solutions it kept, nor how much compute those unsuccessful attempts consumed. The $2,000 figure therefore covers only the visible part of the work.
Noam Brown, a researcher at OpenAI, pointed out that it remains possible to push the compute power used at answer time much further, what’s known as test-time compute, the amount of compute spent while the model reasons through a given question, as distinct from what’s spent training it beforehand. In other words, this result may not yet tap the full potential available.
| Item | Value |
|---|---|
| Compute cost for the ten solutions | About $2,000 (Sol API rates) |
| Number of problems solved | 10 |
| Age of the oldest problem solved | 27 years (posed in 1999) |
| What the figure doesn’t include | Failed attempts and the cost of training the model |
Putting this figure in perspective helps measure the gap. Problems left open for twenty-five or thirty years, ones researchers built entire careers on, solved for a compute cost lower than that of a high-end laptop. It’s this kind of gap that fuels debates about the place AI is taking in jobs once thought safe.
Two caveats apply, though. First, that $2,000 covers the compute, not the training of the model itself, which runs into hundreds of millions of dollars. The figure is striking, but it measures only a fraction of the real economic equation. Second, solving a proof is not the same as knowing what to look for. Choosing the ten problems, the part that gives the result its meaning, still came from humans.
Why Some Mathematicians Are Grinding Their Teeth
In June 2026, the International Mathematical Union endorsed the Leiden Declaration, a text that accuses AI companies of using research work without its authors’ consent and of bypassing peer review, the process by which other researchers examine a piece of work before it’s published. The text specifically targets announcements made by press release rather than in peer-reviewed journals, a practice that, according to its signatories, threatens the integrity of proof and attribution.
The declaration also calls for identifying the tools and compute resources used, and for providing formal proofs whenever possible. On this specific point, OpenAI met the request, at least in part, with its Lean certificates for Astra. This transparency requirement is part of a broader movement to regulate AI labs by institutions, whether academic or public.
The substantive reservations go beyond questions of form. No formal peer review took place, only an informal validation by outside mathematicians. The exact split between what OpenAI Astra produced and what OpenAI’s human team contributed isn’t specified either.
Several of the announced results are counterexamples rather than constructive theory. A counterexample answers a question with no, without explaining why the pattern breaks down, which closes a problem without necessarily advancing understanding. Lean guarantees that the logical steps are consistent with one another, but it doesn’t guarantee that the formalized statement matches the question mathematicians actually had in mind. This limitation is real and often poorly understood outside the circle of specialists.
The OpenAI Astra model remains private. No one outside can test it on other problems, or verify that it reproduces this kind of result, and the question of exact authorship of the results is still an open, unsettled discussion. Terence Tao, one of the most renowned living mathematicians, for his part champions a vision of « big mathematics »: large-scale, decentralized collaborations between humans and machines, the opposite of a closed proprietary model.
0 Commentaires
Aucun commentaire pour le moment. Soyez le premier à commenter !