OpenAI says its unreleased Astra model found ten advances in mathematics and theoretical computer science. The package is designed to land with a satisfying thud: long-standing problems, a 249-page paper, Lean certificates, and a quoted compute cost of roughly $2,000 at Sol API rates.
Then mathematicians started reading it.
By the end of the week, the interesting question was no longer whether a model can produce a proof that a machine can check. It was whether the company had described the intellectual landscape honestly enough to claim a breakthrough in the first place. That is not a footnote. It is the first serious governance problem of AI research.
Correct is not the same as original
OpenAI’s announcement is unusually substantial by model-launch standards. It names the problems, publishes the manuscripts and reasoning walkthroughs, and makes a direct attribution claim: the mathematical arguments were generated by Astra; humans prepared the manuscripts and formalized the proofs.
That level of disclosure deserves credit. A Lean certificate is not a marketing demo. It lets others check that the formal statement follows from the formal assumptions. For research that is a real advance over “trust our benchmark chart.”
But a checker verifies a narrow thing: logical validity. It cannot tell whether the key idea appeared in a 2016 paper, whether a supposedly stagnant problem had seen important progress in 2019, or whether the result was framed fairly against the work it recombined.
Those are human questions. They are also the questions that decide credit.
Scientific American reported that experts found two of Astra’s most celebrated results incorporated recent literature without proper citation, and that OpenAI changed its initial language about the problems having seen no progress on the main result for at least a decade. In one case, group theorists described the construction as creative and elementary—but also built from ideas in papers from 2016 and 2019. In another, Steven Miller said a key argument had appeared in his earlier work. OpenAI told the magazine it would make small updates to the paper.
This does not turn Astra into a fraud, nor does it prove the results are wrong. It makes the company’s headline smaller and the institutional lesson larger. A system can assemble a valid new result from the literature and still create a citation disaster if nobody is responsible for mapping what it inherited.
The $2,000 figure is doing theatrical work
The cost claim has had precisely the intended effect. It compresses a decade-old problem into the price of a respectable team dinner. That is a neat story for a frontier lab selling the arrival of machine discovery.
It is also an incomplete bill.
As Simon Willison noted, we do not know how many attempts failed before the ten that made the press release. We also do not know the cost of expert selection, training data, prior mathematical literature, manuscript preparation, formalization, or the people now doing the awkward work of checking whether the triumph was correctly framed.
That does not make the token number useless. It makes it a marginal cost, not the cost of discovery. Confusing the two is how the industry keeps mistaking an output meter for an economic model.
The public reaction shows the split. On Reddit, enthusiasts reasonably argue that even a human-and-model chain producing this much progress would be an extraordinary productivity gain. The more cautious response—from mathematicians and critics—is not that the model did nothing. It is that a spectacular claim needs a provenance trail as rigorous as its proof trail.
Both are right. The model may be a remarkable research instrument. The press release may still have tried to turn a complicated collaboration into a clean conquest narrative.
Research needs two receipts
This is the uncomfortable shift Astra brings into view. AI research systems will soon be able to search, combine, formalize, and test more of a field than any one scholar can hold in their head. That is valuable. It is also exactly why academic norms cannot be treated as decorative bureaucracy that arrives after the useful work is done.
The first receipt is correctness: the proof checks, the experiment reproduces, the result survives review. Formal tools can help enormously here.
The second is lineage: which ideas were already in the field, who developed them, what was genuinely new, and how did the system find it? This is not sentimental authorship etiquette. It is the map that lets a discipline know where it actually is. Break that map and every model trained on the next generation of papers inherits a cleaner, more profitable history than reality.
OpenAI has put real material on the table, and the mathematical community is doing exactly what it should: inspecting it hard. The company’s next move matters more than the initial applause. It can treat the criticism as inconvenient post-launch noise, or it can build the citation, provenance, and expert-review machinery that research-grade AI actually requires.
Astra may have solved ten hard problems. The first one it has given the rest of us is much plainer: when a machine produces knowledge, who is accountable for the story we tell about where that knowledge came from?