In its announcement, OpenAI said an unreleased internal version of Astra, its next major model, had produced ten results across mathematics and theoretical computer science. OpenAI estimated the token cost for finding all ten solutions at roughly $2,000 at Sol API rates.

Thomas Bloom, a University of Manchester mathematician who runs erdosproblems.com, called the results "big news" in an X post cited by The Decoder, adding that, as mathematical constructions, they were bigger than the unit-distance counterexample OpenAI had disclosed earlier.

Humans used the same model to prepare manuscripts, then had it formalize each argument in the Lean proof assistant. The lab also released model reasoning walkthroughs, a 249-page manuscript dated August 2026 and machine-checkable proof files. The materials give reviewers three separate artifacts to inspect while Astra remains private.

The release extends a test OpenAI disclosed on May 20, 2026, when an unreleased model generated a disproof of the Erdős unit-distance conjecture. In the post, OpenAI also cited a separate program providing 100,000 scientists and mathematicians free access to its best ChatGPT models while it continues to evaluate private systems on open research problems.

What Changed

AI-generated summary, reviewed by an editor. More on our AI guidelines.

The results

The problems range from high-dimensional geometry to lattice cryptography. OpenAI described them in its announcement as questions that had seen no progress on the main result for at least a decade, with most open much longer.

One construction would establish the existence of a non-sofic group. Mathematician Mikhail Gromov introduced soficity in 1999, and The Next Web reported on August 1, 2026, that nobody had proved or disproved the existence of such a group in the intervening 27 years. Another Astra result would disprove Connes's rigidity conjecture, which concerns whether certain groups are uniquely determined by their von Neumann algebras.

The geometry result pushes a high-dimensional sphere-packing bound down to the Cohn-Elkies threshold. OpenAI's August 2026 manuscript calls it the first improvement to the general sphere-packing exponent since 1978. In theoretical computer science, the same manuscript claims an n^4/log n formula lower bound for computing the permanent and n^(1/400)-factor hardness for the Euclidean closest vector problem.

Other results include an exponential parallel repetition theorem for two-player quantum games and resolutions of Erdős problems 146, 180 and 183, according to the list. The announcement also claims improved bounds for binary and spherical codes and a solution to Ehrhart's volume conjecture.

What Lean checks

Lean is a proof assistant. A mathematical argument is translated into formal statements, and the software checks whether each step follows from the definitions and rules encoded in the system. That can catch missing steps or invalid deductions that ordinary prose may conceal.

OpenAI's public repository, created at 06:10 UTC on August 1, 2026, uses Lean 4.32.0 with the mathlib library and Lake build system. Its README gives two commands for downloading cached dependencies and building all certificates. The Apache-2.0 license allows others to inspect and run those files without access to Astra.

A reviewer can clone the project, fetch the cached dependencies with lake exe cache get, and run lake build All to check the certificates against that software stack. The process tests the public proof files on a local machine. It does not provide access to Astra or show how the private model behaves on problems outside this release.

A successful Lean build validates the statement as formalized inside Lean. Journal peer review remains a separate process. Outside researchers cannot test the private model that generated the arguments or determine how mathematicians will rank the importance of each result.

Humans prepared the manuscripts with Astra before the model formalized the arguments, according to OpenAI. Reviewers still have to compare the natural-language claims, the formal statements and the prior literature across each field. The announcement does not include a named outside mathematician who rejects a specific proof.

Responsibility and disclosure

The Leiden Declaration, endorsed by the International Mathematical Union, sets a stricter disclosure standard for AI-assisted mathematics. It asks authors to identify the tools and computational resources used, provide formal proofs where feasible and accept human responsibility for correctness. It also warns that AI-assisted papers can make reviewing more demanding.

The declaration followed the debate around OpenAI's May unit-distance proof. Critics objected that the proprietary model, detailed methods, training data and compute were unavailable outside OpenAI. The Next Web reported on August 1 that the Lean files let anyone with the compiler validate the formal statements without trusting OpenAI or Astra's operator.

OpenAI disclosed Astra's role and an estimated token cost in the post, but the release does not give outside researchers access to the model, its training data or a public testing interface. The public materials allow direct checking of the Lean certificates, while Astra's broader research behavior remains inaccessible. OpenAI has not announced a public release date.

Noam Brown, an OpenAI researcher, supplied his own boundary for the claims. The Decoder reported on August 1 that Brown said the lab had not spent much on each problem and that there were "no Millennium Prize Problems (yet)".

Know someone who'd find this useful? ✉️ Email it to a friend in one click, or they can subscribe free here.

Frequently Asked Questions

What did OpenAI say Astra produced?

OpenAI said an unreleased internal version of Astra produced ten results across mathematics and theoretical computer science.

Why do the Lean certificates matter?

They let reviewers check the formalized proof statements with Lean, but they do not replace journal peer review or give outside researchers access to Astra.

How much did OpenAI say the search cost?

OpenAI estimated the token cost for finding all ten solutions at roughly $2,000 at Sol API rates.

What is the main limit of the release?

The proof files are public, but Astra remains a private model with no public testing interface or release date.

What does the Leiden Declaration add to the story?

The IMU-endorsed declaration asks mathematicians to disclose AI tools and compute resources and says human authors remain responsible for correctness.

AI-generated summary, reviewed by an editor. More on our AI guidelines.

Leiden Declaration Sets AI Proof Rules
OpenAI’s Erdős proof gave mathematicians a real AI milestone. The Leiden Declaration is their answer: disclose the tools, keep humans responsible and make private proofs legible to the field. The fight is over who gets credit, and who gets to check the work.
Implicator.ai
DeepMind AlphaEvolve Scales Math Search, Proofs Need Humans
DeepMind's AlphaEvolve can search millions of mathematical constructions in hours, not weeks. Fields Medalist Terence Tao already builds on its outputs. But the system finds candidates, not proofs. The real shift: math discovery at industrial scale.
Implicator.ai
Mathematicians say AI cracked research proofs. The best tools aren't public
Mathematicians spent a year watching AI move from IMO puzzles to genuine research proofs. Then Harmonic raised $120 million at a $1.45 billion valuation on the premise that formal verification is the moat. The useful tools went private. The academy got the slop.
Implicator.ai
AI News

San Francisco

Editor-in-Chief and founder of Implicator.ai. Former ARD correspondent and senior broadcast journalist with 10+ years covering tech. Writes daily briefings on policy and market developments. Based in San Francisco. E-mail: editor@implicator.ai