Seven Hundred Proofs and No Mathematician

One Word: Power

On October 7, 2026, the Association for Human Mathematics published a four-paragraph statement against the release, the day before, of more than seven hundred mathematical manuscripts generated by an internal OpenAI model. It closed with a line that is likely to stick: the release, it said, was “a demonstration of power” and not an act of scholarship. The text, signed by the association’s communications working group, was picked up within a few hours as a guest post on Terence Tao’s blog, which for almost twenty years has been one of the places where the mathematical community talks about itself. Under that post a discussion opened that is worth reading in full, because almost every possible position on what is happening shows up in it, in raw form.

In this article I try to do three things. The first is to reconstruct the facts with some precision, because the statement assumes a context that people who don’t follow the story closely are unlikely to have, and without that context its claims sound either obvious or incomprehensible. The second is to read the statement as an argument, separating the claims that hold up from those that don’t. The third, which is the one that interests me most, is to use this episode to ask a question that the philosophy of mathematics has been asking for at least half a century and that has suddenly become operational: what does it mean for a problem to be solved when the proof exists, has been checked by a machine, and no human being understands it yet?

Let me state my position up front, out of honesty toward the reader. I work with language models every day and I consider them extraordinary tools. For exactly that reason, I think the AHM’s objections should be taken seriously even where they are poorly phrased, because they touch a structural problem that will soon affect every discipline in which producing results becomes far cheaper than verifying and understanding them.

What Was Released on October 6

On October 6, OpenAI published a vast collection of mathematical results in a GitHub repository, openai/math. The results were produced by an internal frontier model that is not available to the public, and they came with a short post titled Sharing AI progress in mathematics. The figures that circulated in the following days speak of 722 manuscripts grouped into 372 families of results, according to the count reported by Splitfeed, while Nature only mentions more than seven hundred preprints uploaded simultaneously and entirely generated by AI, on problems spanning many areas of the discipline.

In the post, OpenAI says it consulted the Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study and drew on its public recommendations. The repository contains Lean formalizations of many of the proofs, with a commitment to add more as they are obtained, along with a set of materials on the process: ten summaries of the model’s reasoning, estimates of the compute used expressed as ChatGPT Pro usage equivalents, and statistics on the number of problems attempted. The stated average is about three hours of Pro “thinking” per result. The company also announces that it will fund workshops, conferences and programs devoted to understanding the main results produced by AI, and adds that it is still evaluating community-hosted alternatives to GitHub.

Among the manuscripts there are no solutions to the five Millennium Prize Problems that are still open, but according to Nature some of the papers touch on related problems, such as the Hodge conjecture and the Riemann hypothesis. Asked to comment on the value of these results, an OpenAI spokesperson replied that the company will leave it to the community to assess their relevance. The immediate reactions were sharply divided. Some mathematicians celebrated the solution of problems that had been open for decades, others complained of being scooped on work in progress, and a physicist quoted by Nature spoke of a “slopocalypse” even on the assumption that the content turns out to be formally correct. Levent Alpöge, a mathematician who works at Anthropic, acknowledged that there will be sad stories for those who see their projects overtaken, while calling this moment the most significant in the history of mathematics.

Date (2026)	Event
October 7	AHM statement, picked up on Terence Tao’s blog
October 6	OpenAI publishes the openai/math repository; AGMAI note on the release
September 29	The AGMAI publishes guidelines on the responsible release of AI-generated mathematics
September 8	OpenAI announces a solution to the Navier–Stokes problem
September 5	The agent system reaches the solution after about 88 hours
September 1	OpenAI starts the agents on some of the Millennium Prize Problems
August 28	Training of the new internal model begins

The Backstory: Navier–Stokes and the Question of Priority

The AHM statement makes no sense without the September episode, which used up much of the trust that remained between part of the community and OpenAI. On September 8, the company announced that an internal system had produced a solution to the Navier–Stokes problem, one of the seven Millennium Prize Problems set by the Clay Mathematics Institute in 2000, each carrying a one-million-dollar prize. According to the reconstruction published by Unite.AI, OpenAI had started training a new model on August 28, judging it clearly more capable than GPT-6 Astra, its most advanced public model. On September 1, after hearing rumors that two Millennium Problems had been solved, it launched about ten thousand agents on the problem. After 88 hours they reached a resolution, followed by another 17 hours of formalization and verification in Lean carried out with Astra.

A few numbers help show the scale of the operation. The agents reportedly exchanged almost three million messages and generated about 130 billion output tokens, according to ProPakistani, and the published proof runs to 165 pages. It is also worth being precise about what was actually proved. The official formulation of the problem, written by Charles Fefferman, includes four alternative statements: two on existence and global regularity (on the whole space and on the torus) and two on the formation of finite-time singularities in the presence of a smooth external force. OpenAI’s result belongs to the second family and shows a blow-up in which the fluid’s velocity diverges at specific points, and the company itself has acknowledged that the work covers two of the four statements. The Clay Institute has not yet recognized it, partly because its rules require publication in a qualified venue, two years of public standing and broad consensus in the community.

The controversial part concerns priority. Tristan Buckmaster, of New York University, said that he and Levent Alpöge had been working on the same path for almost a year, with a result on the forced Euler equations reached on August 15 and verified in Lean on August 22, and that OpenAI’s interest in Navier–Stokes grew after information about their work reached the company. According to ThePrint, on September 6 he was offered two options: a coordinated publication of the two results one day apart, or a paper written under his name on the Navier–Stokes result with credit given to OpenAI’s model. OpenAI denied having had access to their work or having used user data directly, while admitting that it cannot rule out that de-identified data from the use of its products contributed to training. Sébastien Bubeck publicly rejected the accusation that he had asked for Alpöge’s name to be removed from an announcement.

It is not the job of this article to decide who is right on this point, and the available facts do not allow it. What matters is that the episode showed in concrete terms a risk that until then had been theoretical: a lab with enormous computing power can turn a hint about a human group’s research direction into a complete result in a few dozen hours, making fragile the whole system of incentives built on priority of discovery. Terence Tao, who had called the work a remarkable result, then hosted on his blog, in the following weeks, numerous contributions on the relationship between AI and mathematical research, including some on the formation of singularities in incompressible fluids.

The Rules of the Game According to the Institute for Advanced Study

The Advisory Group on Mathematics and Artificial Intelligence (AGMAI) is the body to which the AHM accuses OpenAI of having attributed a legitimacy it did not have, so we need to look carefully at what it actually said. The group is made up of nine top-level mathematicians, including Timothy Gowers, Martin Hairer, Edward Witten, Camillo De Lellis, Ravi Vakil and Melanie Matchett Wood. It began with a request from OpenAI to some of them to form an external advisory committee. The members turned that request, with the company’s agreement, into an independent, unpaid group willing to advise any lab.

The guidelines of September 29, built on more than six hundred responses to a survey of the community, open with an explicit distancing. The members state that they do not endorse the practice of testing advanced mathematical problems on proprietary models inaccessible to the rest of the community, and they ask labs to stop. They specify, however, that the recommendations that follow are written with the fact that the practice exists in mind. The foundation of the document is an old norm of the discipline: the authors of a paper must understand its argument, have verified its correctness and take full responsibility for it, then present it in seminars and conferences. Three principles follow. Significant results should be released responsibly and early. Whoever releases mathematics that no one yet understands should take on, financially too, the process that will lead to understanding. And that process should remain organic and guided by the community, not by the labs.

The operational recommendations for work that no human being has yet understood are specific and verifiable, and this lets us compare them with what OpenAI actually did on October 6. The table below is my own reading, based on OpenAI’s post and on the AGMAI text, and it does not replace the examination of the repository that the community is carrying out.

AGMAI recommendation	What OpenAI did	My assessment
Cite the literature containing ideas related to the proofs	Commitment to improve citations and exposition in future releases	Postponed
Rewrite the proofs in the style of a traditional mathematical paper	Same commitment for the future; review protocols in the repository	Postponed
Deposit the work in archives not controlled by labs, with persistent identifiers	Published on GitHub; community alternatives still under consideration	Not met
For each result, disclose the model, prompt, summarized chain of thought, timing and costs	Ten summaries of the reasoning, aggregate compute estimates	Partial
Formalize as much as possible, stating the formalization status	Lean for many proofs, others coming	Largely met
Document how many similar problems were attempted without success and how they were chosen	Statistics on the problems attempted	Partial, to be verified
Fund understanding through existing nonprofit institutions, without directing it	OpenAI announces it will fund workshops and programs	Ambiguous on the key point

The last row deserves a comment, because it is where the gap between the letter and the spirit is subtlest. The AGMAI asks that the choice of which activities to support be made by nonprofit institutions that already have established procedures, precisely to avoid the lab that produced the results also deciding which of them deserve to be understood. OpenAI’s announcement, instead, speaks of programs funded by the company without specifying who will govern them. The AGMAI document also asks labs not to use the release of mathematical results as a marketing vehicle, pointing to the negative externalities this practice dumps on the community.

On the same day, October 6, the AGMAI published a very measured note. The group calls the release an important event. It makes clear that its advisory role should not be read as a judgment on the value of the results, nor as an endorsement of the process by which they were obtained. And it adds an observation that I consider the most important of the whole affair: the future of mathematical research cannot be reduced to understanding the results produced by labs, because mathematicians must be able to formulate their own questions and explore directions that nobody has chosen as a showcase for a system’s capabilities.

The AHM statement, read closely

The Association for Human Mathematics presents itself as an organization that defends mathematics as a human enterprise against the threat of artificial intelligence, and defends the community’s independence from corporate interests. It says it wants to avoid complicity with an industry whose social, environmental and economic impacts it condemns. It is an openly militant position, one that calls for individual action and large-scale coordination, and that identifies teaching, journals and the training of young people as the most vulnerable points of mathematical institutions. The statement should be read in this frame, as a political act before it is an analysis.

The text contains four distinct argumentative moves, and it is worth examining them separately, because they differ greatly in strength.

The first move is the opening, which recalls that OpenAI is defending itself in lawsuits over plagiarism, copyright infringement and trademark dilution. It is the weakest part of the text. The copyright litigation has no logical connection with the correctness or value of a proof, and putting it before the main argument has the effect of poisoning the well before saying anything on the merits. Several commenters on Tao’s blog noticed this right away. One reader, who said he was not a mathematician, observed that mathematics is one of the few fields where the work can be checked, by hand or by computer, and that a correct proof does not become incorrect because of a civil suit.

The second move claims that mathematicians did not ask for this work, and that OpenAI, by ignoring the central premise of the AGMAI, showed total disregard for the norms of scientific research. There are two problems here. The first is representation: no association can speak for mathematicians as a whole, and indeed among the comments there are people who say they are happy to have in front of them a text that might contain the proof of problems they work on, and people who point out that not even Perelman was commissioned by the community to prove the Poincaré conjecture. The second is chronological: the AGMAI’s invitation to stop testing advanced problems on proprietary models dates to September 29, while the work released on October 6 had evidently been carried out earlier, as another commenter pointed out. One can argue that OpenAI should have waited, but describing the release as a deliberate violation of a premise that did not yet exist when the work was done is a stretch.

The third move is the claim of a vision of progress that belongs to mathematicians, informed by history and by considerations specific to the discipline, in the name of which the AHM rejects the idea that the release advances the field. This thesis is more interesting than its wording suggests, and I will come back to it in the philosophical part, because behind it lies a precise conception of what mathematical progress is, which the statement unfortunately does not spell out.

The fourth move is the closing line about power, which is both the most rhetorical and the truest. Releasing seven hundred files in a single day has effects that don’t depend on whether each file is correct. It abruptly shifts the agenda of entire fields, forces those who were working on these problems to rethink years of projects, and imposes on the community a verification burden that nobody agreed to. In this sense the show of power is real, and it comes down to an asymmetry between those who can generate results with thousands of agents and those who have to read them one by one. The final call to cut all collaboration with OpenAI, on the other hand, is a political choice that the text never argues for, and it risks shutting out of the discussion the very mathematicians who would have the strongest standing to demand better conditions from the labs.

To sum up, the statement is right about the problem and wrong about almost all the reasons it gives. The problem is the concentration of the capacity to produce mathematics in a few private actors who decide which problems to tackle, when and how to publish, and who has to pay the cost of understanding. The reasons offered, namely the copyright dispute, the claim to speak on behalf of everyone, and the casual reading of the timeline, weaken a position that deserved better arguments.

What a Lean Formalization Really Guarantees

A proof formalized in Lean guarantees that a given formal statement follows from certain axioms according to the rules of a logical system. That guarantee is extraordinarily strong within its boundaries, but the boundaries are narrower than public debate tends to acknowledge. Those who defend the OpenAI release lean heavily on the formalizations, and rightly so, because they are the sharpest difference between this wave of results and the informal proofs generated by models up to a year ago. So it is worth understanding precisely what they certify.

Lean 4 is built around what is called the de Bruijn criterion. Tactics, automation and any component that helps build the proof can be complex and even unreliable, because in the end everything is translated into a type theory term that a small, independent kernel checks. If the kernel accepts the term, the statement is proven with respect to the axioms used, and this holds regardless of whether the term was written by a human being, by a language model or by ten thousand agents exchanging three million messages. This property is what makes mathematics the ideal terrain for AI systems, because it offers an external verifier that is cheap and cannot be manipulated by the system producing the solutions.

Still, there are at least four points where the formal guarantee does not reach, and each one corresponds to a concrete way in which a formalized result can nonetheless be wrong or misleading.

Incomplete proofs. In Lean the keyword sorry lets you leave a hole in the proof and still have the file compile. A serious check requires the count of sorry to be zero for the main results, and a human audit of the ten results that OpenAI released in August reports exactly this figure for all ten, pinning the reference to a specific commit and to Lean 4.32.0.
Additional axioms. Beyond the standard axioms of the library, namely propositional extensionality, classical choice and quotients, a file can declare its own axioms, and an axiom that asserts the claim makes it trivially proven. The command that lists the axioms a theorem depends on is the first check to run on every artifact.
Fidelity of the statement. This is the most serious problem and the least discussed. Lean verifies that the proof proves the formal statement, not that the formal statement matches the mathematical problem it claims to have solved. A slightly different definition of regular solution, function space or boundary condition can turn an open problem into an exercise, and for partial differential equations, where definitions are delicate, the risk is real. This is why AGMAI asks for a challenge file to be compared with a comparator, and for metadata linking the informal text to the formal artifacts.
Accepted dependencies. Many formalizations are complete only up to standard results taken from the literature and not yet present in Mathlib. This is a legitimate practice as long as it is declared, but it means the certification is conditional, and the audit I cited stresses precisely the need to distinguish reconstructed arguments from accepted dependencies and from questions that remain open.

The same audit recalls an instructive precedent, OpenAI’s First Proof exercise, in which an attempt initially considered probably correct was reassessed after criticism from experts and the community. The lesson is that formal verification drastically reduces the space of error but also moves it, concentrating it in the translation between informal mathematics and formal language, which remains human work, slow and highly specialized.

There is also a point about scale. For a single proof, a small group of experts can check statements, axioms and dependencies in a reasonable time. For seven hundred manuscripts spread across dozens of fields, each with its own formal conventions, checking the fidelity of the statements becomes a collective project of unprecedented size. As of this writing, there is no public, independent inventory of which results in the repository are fully formalized, which partially and which not at all. In my view, this is the first thing the community should demand.

What It Means for a Problem to Be Solved

The philosophical question raised by OpenAI’s release is whether a correct, certified proof that no one understands solves a problem in the sense in which mathematicians have always used that word. The question seems new, but the philosophy of mathematics has been discussing it since at least 1976, and retracing the stages of that discussion helps explain why the AHM, even while arguing badly, touches a raw nerve.

In 1976 Kenneth Appel and Wolfgang Haken proved the four color theorem by reducing it to a very large set of configurations checked by a computer. Three years later Thomas Tymoczko argued that this proof introduced an empirical element into mathematics, because no human being could go through it in its entirety and its acceptance depended on trust in an experiment, that is, in the correct functioning of a machine. Tymoczko was taking up an idea of Wittgenstein, who in his remarks on the foundations of mathematics had insisted that a proof must be perspicuous, something that can be taken in at a glance, and that a procedure that cannot be mastered in this way has a different status. Today the four color theorem is formalized, and its status is no longer in question, but the distinction between knowing that a statement is true and understanding why it is true has remained.

In the same year, 1979, Richard De Millo, Richard Lipton and Alan Perlis published a famous article on social processes and proofs, in which they argued that a theorem is accepted at the end of a collective process made of reading, discussion, reformulation, use in other contexts and growing familiarity, and that mathematical certainty is the product of this process more than of a formal derivation. The authors drew a skeptical conclusion about the formal verification of programs, which the following decades have partly disproved, but their description of how the mathematical community works remains accurate. The release of seven hundred manuscripts in one day skips exactly this process, because it delivers results that arrive already certified by a machine but that no community has yet digested.

The text that best illuminates the AHM’s position, however, is William Thurston’s 1994 essay on proof and progress in mathematics, written in response to a proposal by Arthur Jaffe and Frank Quinn to separate rigorous mathematics more sharply from speculative mathematics. Thurston argued that the product of mathematics is human understanding, and that proofs are the vehicle through which this understanding is built and transmitted. He told how some of his results on 3-manifolds, proved correctly but communicated badly, had in effect left the field barren for years, because no one could make them their own and build on them. If we take this view seriously, a theorem that is proved but not understood is incomplete progress, because it adds a true statement to the inventory but adds no capability to the community that is supposed to use it.

The case closest to today’s, though, is Shinichi Mochizuki’s inter-universal Teichmüller theory, with which he has claimed since 2012 to have a proof of the abc conjecture. For more than a decade the main difficulty has been communicating the argument, even before judging its correctness at any specific step, and when Peter Scholze and Jakob Stix identified what they considered a critical point, the discussion stalled in a disagreement that the community has no tools to resolve without a shared understanding. Mochizuki’s case shows that a proof that a single mind, human or artificial, considers complete is not enough, because mathematical knowledge is a public fact.

Formal verification changes this picture at one specific point and leaves it intact at another. It changes it because it makes certification independent of understanding, and so it eliminates the Mochizuki scenario as far as truth is concerned, since a Lean kernel does not need to be convinced. It leaves it intact because the other two functions of proof, the explanatory one and the transmission of techniques and concepts, remain entirely to be carried out. In Proofs and Refutations, Imre Lakatos showed that proofs generate new concepts, refine definitions and bring out the counterexamples that correct the statement, and that this very dynamic is the engine of the discipline. A commenter on Tao’s blog put the question very concretely about Navier–Stokes, asking whether after OpenAI’s result we understand fluids better than before, and in particular whether we know why the construction requires a smooth forcing term and whether this is an obstacle to the case without forcing.

The comparison with chess and Go, which several commentators have proposed, is useful precisely because it is imperfect. When AlphaGo surpassed human champions, the value of the game was not destroyed, because Go produces nothing outside itself and its value lies in playing it. Mathematics, instead, produces concepts that migrate into physics, computer science and engineering, and it does so precisely through the human understanding of the mechanisms that make a proof work. A result that is true but opaque can be used as a black box, the way a physicist uses a theorem without knowing its proof, but it does not generate the lineage of ideas that usually accompanies the solution of a great problem. One might object that this lineage will come anyway, once the community has assimilated the results, and for many of them that is probably so. But assimilation has a cost, and the question of who pays it is the point where philosophy becomes economics.

Who Pays the Cost of Understanding

The material heart of the story is a disparity in cost between those who produce results and those who have to verify and absorb them. This disparity explains, better than any argument about the purity of the discipline, why the release was perceived as a show of force. According to OpenAI, the average result required the equivalent of about three hours of ChatGPT Pro reasoning. The human cost on the other side is of a completely different order of magnitude. Suppose, as a working hypothesis and not as a measured figure, that a serious review of a research paper on an open problem takes between twenty and forty hours of a specialist’s time. Seven hundred and twenty-two manuscripts then amount to roughly fifteen to thirty thousand hours, that is, ten to twenty person-years of expert work, before even counting the time needed to understand the results well enough to use them.

Anyone who works with generative systems recognizes this structure, because it is the same one we see in code, in documentation and in every domain where producing has become cheap and checking has stayed expensive. In mathematics the disparity is softened by formal verification, which hands the checking of logical correctness over to a machine, but it does not disappear. As we have seen, the fidelity of the statements, the verification of dependencies and above all understanding remain in human hands. And these people are largely university researchers, whose time is funded by public money and whose refereeing work, by custom, is unpaid.

The sociology of science offers a useful tool for reading the situation. Robert Merton described the ethos of science through four norms: communism of knowledge, meaning the common ownership of results, universalism of the criteria of judgment, disinterestedness and organized skepticism. He also observed that the reward system of science revolves almost entirely around the recognition of priority. OpenAI’s release formally satisfies the first norm, because the results are public and free, and it supports the fourth thanks to the formalizations. It is fragile on disinterestedness, though, given that the AGMAI itself felt the need to ask the labs not to use mathematics as a marketing tool. Above all, it alters the system of priority: an actor who can attack hundreds of problems in parallel makes it unpredictable, for a young researcher, whether years of work will be anticipated within a single afternoon. The Buckmaster–Alpöge case, however one judges it, has made this risk visible to everyone.

A second asymmetry adds to this one, and it concerns access to tools. The AGMAI wrote that the use of proprietary internal models risks creating a two-tier system in which the labs run faster than the rest of the field, alienating the mathematical community from its own discipline. It added that even with public models, unequal access, due to economic and institutional reasons, risks deepening the inequalities that already exist between rich and poor universities. Here the problem stops being specific to mathematics. When the ability to produce knowledge depends on access to computational resources that only a few private actors own, the question of who decides which problems deserve attention becomes a question of research governance. Mathematics is simply the first field where it arises so sharply, because it is the one where automatic verification is most mature.

In fairness, the opposite argument should be reported too, since it was expressed clearly under Tao’s post. OpenAI will not stop working on mathematics, both because it is an ideal testbed for systems able to improve their own reasoning, and because nobody has the right to prevent someone from working on a problem. The realistic alternatives are therefore two: keep the results private, or make them public so the community can examine them. The second is clearly preferable for science. I find this argument hard to reject. The point, though, is that between secrecy and the release of seven hundred files all at once there is a wide space of intermediate approaches: staggered, agreed upon with scientific societies, accompanied from the start by resources for verification. It is in that space that the AGMAI’s recommendations tried to steer the labs.

Three Words Instead of One

The conclusion I draw from this story is that the word “solved”, applied to a mathematical problem, is about to split into three distinct meanings, and that much of the clash between the AHM and those who defend OpenAI comes from each side using a different meaning without noticing. The first meaning is certification: the existence of a proof checked by a formal verifier, with a faithful statement, no gaps and no extraneous axioms. The second is understanding: the presence of at least one person able to explain why the argument works, where the decisive steps are and what prevents going further. The third is integration: the moment when the ideas of the proof have become part of the community’s heritage and generate further work.

Until a few years ago these three states almost always coincided, because the only way to get the first went through the second, and the third followed with time. Today AI systems make it possible to get the first without the second, and the release of October 6 made it clear that the community needs a vocabulary and institutions that can keep the three levels apart. Those who celebrate the release as the most important moment in the history of mathematics are talking about the first, and for many of the results they are probably right. Those who reject it as a show of power are talking about the second and the third, and they are right too, because neither has been reached, and the cost of reaching them has been passed on to others without any agreement.

If I had to say what the mathematical community could realistically demand, without boycotts that risk leaving it out of the room, I would point to three things. The first is an independent, public inventory of the status of every result released, with an explicit distinction between complete formalization, conditional formalization and no formalization, and with human checking of whether the statements are faithful. The second is the deposit of the work in archives run by the community, with persistent identifiers and revision history, as the AGMAI asks. The third is that the funds for understanding be entrusted to nonprofit bodies with their own procedures, so that the choice of which results to study stays in the hands of those who study them.

One question remains that no release rule can settle, and the AHM statement, for all its limits, deserves credit for raising it. If the ability to find proofs becomes abundant and cheap, the value of human mathematical work will have to shift toward what stays scarce: choosing the questions, building concepts, explaining and connecting. This is what Thurston argued thirty years ago, when no machine could prove anything, and it is curious that it took a machine able to prove almost everything to make it obvious.