OpenAI’s post says an internal model, described as a forthcoming major system, helped produce ten advances across pure math and theoretical computer science. Several came with papers, Lean formalizations, and model-written reconstruction notes. The claim is not just that the model solved textbook exercises. It is that it made publishable progress on long-open problems, including results in areas like sofic groups, Connes rigidity, sphere packing, Ramsey theory, and circuit complexity.
The strongest signal was that people who knew specific areas did not dismiss the work as fluff. Comments from readers familiar with the problems said at least some of these are genuine breakthroughs, not toy tasks, and that a few would be career-defining if done by a human researcher. A recurring point was that math is a natural proving ground for frontier models because correctness is unusually checkable. That makes it attractive both for training and for public demos. It also explains why labs keep showing math before law, biology, or policy. The bigger pattern many readers saw is that AI is moving fastest in domains where outputs can be verified, whether by tests, proof assistants, or clear objective criteria.
But almost every serious reaction came with a calibration warning. The most common objection was not that the results are fake. It was that OpenAI disclosed outcome more clearly than process. People wanted to know how many problems were attempted, how many failed, how much human expert prompting and triage happened, and whether the touted per-problem cost hides a much larger search budget. Several commenters said the right comparison is not just token cost. It is the full system cost of expert operators, orchestration, and repeated runs. That matters because the headline can mean either “a model can now reliably solve major open problems” or “a well-funded lab can occasionally extract wins by throwing a large research stack at many targets.” Those are very different capability claims.
The other major caution was about what Lean verification does and does not guarantee. A checked Lean proof is far stronger than an ordinary informal paper on syntactic correctness, but it does not prove that the theorem statement encoded in Lean is the theorem mathematicians care about. Humans still have to audit that translation, and recent examples of
proof assistant bugs made people wary of treating
formalization as magic dust. So the consensus landing point was sharper than both the hype and the dismissal. These results likely show real frontier capability in formally verifiable research. They do not yet show that models can independently build broad mathematical theory, explain their own discoveries in a way experts can reuse, or generalize cleanly to messier high-value fields.
That distinction fed a second theme about what kind of research is being automated first. Several commenters argued that many of the listed wins are counterexamples, bound improvements, or combinatorial constructions rather than the creation of a new theory in the
Grothendieck sense. Others pushed back that this still understates the achievement, because finding one decisive
counterexample to a famous conjecture can unlock an entire field. The practical synthesis was that AI is already good enough to change how top researchers work, especially when the task is to search broadly, connect distant techniques, and grind through huge structured spaces humans cannot. What remains scarce is explanation, taste, and agenda-setting. Humans still decide which questions matter, how to interpret the answers, and how to turn isolated results into a program rather than a pile of proofs.
openai.com
Gary Marcus follow-up on Astra claims