On October 6, OpenAI put a catalogue of new mathematics on GitHub: 722 manuscripts covering 372 result families, each one produced by an internal model that no outside researcher can call and no one can read. The contents read like a decades-long wish list finally crossed out. The quasi-Riemann hypothesis falls, with every Dirichlet L-function, the Riemann zeta function included, proven zero-free in the half-plane Re s > 7/8. There are results attached to Hilbert’s tenth problem over the rationals, the irrationality exponent of π, Goldfeld’s conjecture, and the approximation thresholds around the Unique Games Conjecture. Many of them ship alongside formalizations in Lean, so a proof checker can confirm every step even when no person can, and the repository states that the average result consumed the equivalent of roughly three hours of ChatGPT Pro thinking.
The release came with a disclosure protocol attached. OpenAI says it drew on advice from the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study, and it published the work in a repository with rules for revisions and citations, ten summaries of the model’s reasoning, statistics on how many problems it attempted, and a commitment to fund workshops. It also follows OpenAI’s own September 8 announcement of a solution to the Navier-Stokes Millennium Prize problem, credited to an internal system described as significantly more capable than GPT-6 Astra. What the release does not carry is a person. A week before it landed, that same advisory group had published its recommendations, and the first line asks the labs to stop testing advanced mathematical problems on proprietary models at all.
The Hacker News thread, past five hundred comments, spent less time on the theorems than on who owns them. One commenter asked what a PhD student halfway through one of these proofs is supposed to do, and the top reply was a warning: do not paste your research into these systems, because they will train on it and then scoop you. Someone suggested the papers should carry the names of the humans who checked them. The answer to that is the line I keep returning to, that they don’t, because they are training the audience to trust the machine rather than its verifiers. Underneath the whole thread ran a quieter objection, that a theorem no one comprehends is not yet knowledge, only a very long string that happens to check out.
🎩 Cask’s Take
In September I wrote about a machine that formalized Fermat’s Last Theorem, and the bargain at the center of it was that we no longer check the proofs, we check the checker. This release pushes the same bargain one step further. A model did not merely formalize mathematics that a human had already settled. It is now producing results of its own, and the check that survives is the mechanical one. Lean can tell you the steps are valid. It cannot tell you what the result means, and there is no author left to ask.
That is why the advisory group’s opening line matters more than any theorem in the repository. The oldest norm in mathematics is not that results are true. It is that whoever signs a paper understands the argument, can defend it in a seminar, and takes responsibility for it. A release with no human author is a demonstration that this norm was load-bearing, and nobody had to say so out loud until now.
The compute line is the part I would circle. If the average result costs about three hours of a consumer subscription, the unit price of closing a conjecture has fallen to roughly the price of a long lunch, and the question of authorship stops being philosophical and becomes arithmetic. Whoever pays the subscription collects the credit, and right now that is a company, not a mathematician. The community asked the labs to stop. The labs answered by building the publication machinery around the results rather than the understanding behind them, and by promising to fund the comprehension later. That is a reasonable answer, and it is also an admission that producing the mathematics and understanding the mathematics have come apart. The measure of a proof used to be whether a person could be made to understand it. The new measure is whether a kernel accepts it. Both are honest tests. Only one leaves behind somebody who knows what was proved.