On October 6, OpenAI pushed 722 manuscripts to GitHub. They contain 372 groups of results from an unreleased internal model, and OpenAI says each one resolves or substantially advances an open problem in math or theoretical CS.
It's the top story on Hacker News with 1,400+ comments. Scott Aaronson called it "one of the biggest days in mathematical history." A day later, the Association for Human Mathematics told its members to stop collaborating with OpenAI.
Both reactions can be right. If you ship AI-generated code, this fight is your future, so it's worth understanding.
What actually shipped
From the coverage (The Decoder, Scientific American, Aaronson):
- Cost per result: about 3 hours of ChatGPT Pro-equivalent compute on average. Most results came from a single prompt to a single agent.
- Contrast: the earlier Navier-Stokes result reportedly took a swarm of 10,000 agents and millions of dollars of compute. Per-result cost fell by orders of magnitude.
- Targets named in the coverage: Unique Games Conjecture, L=BPL derandomization, sub-O(n log n) integer multiplication, matrix multiplication improvements, an area law for 2D gapped Hamiltonians, the four-dimensional Kakeya conjecture, and "progress toward" Riemann. These are career-defining problems.
- Verification: many proofs ship with Lean formalizations, plus reasoning traces.
- Not solved: P≠NP. Aaronson points out the pile doesn't contain the big separations.
Aaronson cites a rough ~5% success rate over the problems attempted. I'd treat that as his estimate. The sources I read disagree on the exact number of attempted problems.
The part that should worry you: nobody can replicate it
The model is unreleased. You get the outputs, not the machine.
MIT's Andrew Sutherland: until the model is released and people can replicate, claims about one-shotting problems with a single agent should be treated as unverified.
An independent advisory group reportedly asked OpenAI to release the model, the exact prompts and per-problem compute. Scientific American says OpenAI isn't fully following those recommendations.
If a startup demoed a "10x faster compiler" this way, you'd ask for the repo and the benchmark harness. Same standard.
"But it's in Lean" doesn't close the question
Lean checks that a proof is logically valid for the statement as formalized. It doesn't tell you:
- Whether the formal statement matches the problem people care about.
- Whether the result is novel.
- Whether a human can understand why it's true.
Type-checking passing is not the same as the code doing what the product manager meant.
Item 3 is the pain point. Dana Moshkovitz, whose career centers on Unique Games, described the UGC proof's exposition as reading like something written "by someone who's on psychedelics" (via Aaronson). A proof can be correct and still not transfer any understanding.
There is real evidence the output is good
The data so far is better than the hot takes suggest. A human audit of OpenAI's earlier August 1 batch (ten principal results, 18 chapter-level reviews) found no confirmed substantive mathematical error in a principal result. Review depth varied. One "polarity error" turned out to be a missing overbar lost in PDF extraction.
Independent follow-ups were mixed:
- Connes's rigidity conjecture was confirmed false using one chapter's mechanism.
- A hardness theorem got strong corroboration.
- Another infinite-family result hasn't been independently replicated yet.
So the realistic read: mostly right, unevenly checked, and the checking is the bottleneck. That's the same shape as a codebase where 90% of PRs are agent-authored.
Why mathematicians are furious anyway
The AHM statement says mathematicians didn't ask for this, that it contradicts the advisory group's guidance, and that bulk-releasing 700+ files is "a display of corporate power" rather than scholarship. It urges the community to stop collaborating with OpenAI.
Per Scientific American, 25 Fields Medalists signed a letter warning that mass-producing true statements could destroy fertile ground rather than bring new ideas to life. Tim Gowers worries that within one to two decades the literature could grow so fast that no human community truly understands it.
Daniel Litt takes the other side: if we want the answers, why ask the company to keep them secret?
Strip the politics and it's a classic producer/reviewer asymmetry. Generating a candidate proof now costs hours of compute. Verifying, contextualizing and maintaining it costs scarce expert attention. It's a pull request flood with no CODEOWNERS.
What I'd take from this as an engineer
- Generation is now cheap. Adjudication is the product. Whoever builds good review tooling (formal checks, reproduction, provenance) wins. Another paper in the wild frames this as "verification abundance, adjudication scarcity."
- Machine-checkable specs beat vibes. Lean is the extreme case. In your stack that's property tests, contracts and types that pin intent, not just coverage numbers.
- Unreproducible results are marketing. Release the harness, the prompts and the cost, or expect pushback from the experts you need on your side.
- Dumping beats nothing, but it's not collaboration. The backlash is about process, not about whether the math is true.
Unverified: the "withdrawn" results
A tweet claiming OpenAI withdrew three mathematical results is also on the HN front page. I couldn't load the post, and nothing else I found corroborates it. I'm not going to guess at details. If it's confirmed, it's the strongest argument yet for why a review pipeline has to exist before the release.
Bottom line
The numbers say the capability is real, and the audits so far support that. The protocol is what's broken. Software engineering is about five minutes behind math on the same curve, so watch how this ends.
Sources: the linked articles above, plus the Hacker News discussion. Figures are as reported there and some conflict between outlets.
Top comments (0)