On August 1, 2026, OpenAI announced its next major model family, Astra, by doing something unusual for a product launch: dropping ten machine-verified solutions to long-standing open problems in mathematics and theoretical computer science. Each result came packaged with a model-written reasoning walkthrough, a human-prepared manuscript, and a Lean 4 proof certificate hosted on GitHub under an Apache 2.0 license. The GitHub repository reports a "sorry" count of zero, meaning no step in any of the ten formalized proofs has been left unproven. That detail matters because the mathematical community has consistently raised one objection to AI-generated proofs: they are hard for outsiders to independently check. A Lean 4 certificate sidesteps that objection entirely. Anyone with the Lean compiler can verify the results without trusting OpenAI or its model.
The scope of problems spans high-dimensional geometry, coding theory, group theory, quantum complexity, lattice cryptography, and extremal combinatorics. OpenAI published a 249-page manuscript collection alongside the certificates. Noam Brown, one of the researchers behind Astra's test-time reasoning technology, noted on X that the total compute cost to find the solutions would run roughly $2,000 at Sol API rates, and then added, pointedly, that OpenAI "didn't spend a lot on each problem" and that it is "possible to push test-time compute much further." He called Astra a "major step for scientific reasoning." Sébastien Bubeck, OpenAI's Head of Mathematics Research, described each result as "beautiful" on X, noting the combination of Lean certificates and chain-of-thought walkthroughs. None of the ten results has been through peer review as of the release date, a fact worth holding onto given what happened in October 2025, when OpenAI's then-vice president of science Kevin Weil claimed GPT-5 had solved ten previously unsolved Erdős problems, a claim that was later publicly challenged.
The three results that have drawn the most attention from working mathematicians are the construction of a non-sofic group, the disproof of the Connes Rigidity Conjecture, and a new upper bound on high-dimensional area packing. Each of them has sat open for decades. Each is a different flavor of hard.
The headline result is the first-ever explicit construction of a non-sofic group, resolving a central question in group theory that has been open since Mikhail Gromov introduced the concept of soficity in 1999. For 27 years, no mathematician managed to prove or disprove whether non-sofic groups even exist. To understand why that matters, it helps to know what sofic means. A group is sofic if its behavior can be approximated arbitrarily well by finite permutation systems. All amenable groups and all residually finite groups satisfy this condition, which covers essentially every group that shows up in day-to-day mathematical practice. The question of whether every countable discrete group must be sofic was one of modern group theory's most prominent unanswered questions. Astra's construction answers it: no. Thomas Bloom, the University of Manchester mathematician who curates the Erdős problems catalogue at erdosproblems.com, called the results "big news" on X and rated them more significant than the unit distance counterexample OpenAI published three months earlier, in May 2026. "Maybe not bigger than a proof of unit distance would have been," Bloom wrote, "but in terms of constructions, this is big." That comparison to the unit distance result is itself telling. OpenAI had already disproved the Erdős unit distance conjecture, an 80-year-old problem in discrete geometry, before this release. The non-sofic group construction is, by Bloom's read, the more important construction of the two.
The second result is a disproof of the Connes Rigidity Conjecture, posed by Fields Medalist Alain Connes in 1980, which means this one had been open for 46 years. The conjecture lives at the intersection of group theory and operator algebras, specifically von Neumann algebras. A group is a discrete algebraic object: its elements multiply according to rules. A von Neumann algebra is an analytic object built from how that group acts on a Hilbert space. Connes conjectured that for sufficiently rigid groups, the analytic shadow, the von Neumann algebra, would uniquely determine the original group. The conjecture held intuitive appeal because rigidity felt like it should transfer. OpenAI's manuscript constructs a disproof by producing infinitely many pairwise nonisomorphic property-(T) groups that share the same group von Neumann algebra. In plain terms: different groups, same analytic fingerprint. The conjecture is false. Property-(T) groups are among the most rigid groups mathematicians know, which is precisely what makes the result surprising. The very setting where Connes's conjecture seemed most likely to hold is where Astra found the counterexamples.
The third result is a new upper bound on high-dimensional area packing, and it comes with a specific historical timestamp: the previous record on the general upper-bound exponent had stood since 1978, set by the Kabatiansky-Levenshtein method. Area packing asks how densely equal non-overlapping spheres can fill space. Dimensions 8 and 24 have celebrated exact answers, but the general high-dimensional problem is largely controlled by competing upper and lower bounds that researchers have spent decades trying to tighten. According to OpenAI's official announcement, the Astra manuscript pushes the general area-packing upper bound down to the Cohn-Elkies threshold, which OpenAI describes as the first improvement to the general area-packing exponent since 1978. That is a 48-year gap between records. The Cohn-Elkies threshold had been a natural target because the Cohn-Elkies linear programming method is the sharpest general tool available, but reaching that threshold as a provable upper bound had resisted prior efforts.
What separates this announcement from a typical research paper is the combination of scale and verifiability arriving together. Ten results, 249 pages of manuscripts, and a zero-sorry Lean 4 proof repository released simultaneously is not how mathematical knowledge normally accumulates. It usually arrives one result per paper, refereed over months or years. The Lean certificates address the verification gap directly, but the peer review gap remains real. The mathematical community has been watching this pressure build. In June 2026, the Leiden Declaration, endorsed by the International Mathematical Union, warned that AI companies are using published research without consent, bypassing peer review, and threatening the integrity of proof and attribution, specifically calling out companies that announce results through press releases rather than peer-reviewed journals. That declaration landed six weeks before the Astra release. Fields Medal winner Timothy Gowers, reflecting on an earlier model's performance, warned of the "possible destruction of mathematical culture" if mathematicians stop building the expertise needed to understand these results themselves.
Brown was also candid about Astra's limits. OpenAI tried and failed to crack any of the seven Millennium Prize Problems, each of which carries a $1 million prize from the Clay Mathematics Institute. Only one has ever been solved since the prizes were announced in 2000. "Sadly, no Millennium Prize Problems (yet)," Brown wrote on X. The parenthetical is doing real work there. The framing on Astra's positioning is also unresolved: according to The Information (reported by ForkLog), Astra will sit as a separate model class alongside Sol, Terra, and Luna, and OpenAI has not decided whether it will be released as GPT-6 or within the GPT-5 lineup. No release date has been set. What OpenAI has done instead is use the ten math results as the announcement itself, letting the proofs speak before the product ships. Given what happened with the October 2025 Erdős claim, the decision to anchor this release in machine-checkable Lean certificates rather than verbal assertions looks like a deliberate correction. The math community can argue about peer review. It cannot argue with a zero-sorry proof file.