OpenAI says an internal model solved ten decade-old math problems

OpenAI says it pointed an internal version of its next large model, called Astra, at ten mathematics problems that had gone at least a decade without progress on their main result, and the model found solutions to all of them. Each one cost under $2,000 in compute. To back the claim, OpenAI published Lean 4 formalizations and accompanying papers in a public GitHub repository, so other mathematicians can check the proofs instead of taking the results on trust.

Simon Willison, who flagged the announcement, is not fully persuaded by the presentation. He points out that OpenAI did not release the prompts used to reach these solutions, which makes the work harder to reproduce and leaves open how much human steering went into each one. He also sets two reactions from mathematicians side by side. One describes a profound spiritual crisis for a field built on human insight, while Terence Tao offers a calmer reading he calls "big mathematics", where people supply the questions and creative direction and machines do the technical grind.

The part worth holding onto is the cost. If a frontier model can close decade-old problems for a few thousand dollars each, the bottleneck in parts of pure mathematics moves away from raw difficulty toward which problems are worth pointing a model at, and who checks what comes back.

Why it matters

If you work in mathematics or any proof-heavy field, the live question is no longer whether a model can contribute but how you verify what it produces. The Lean formalizations are the part to read before trusting any single result, and the missing prompts are a fair reason to stay skeptical for now.