The field of mathematics is in turmoil, thanks to AI. <\/p>\n\n\n\n
As the field advanced, one of the techniques mathematicians leveraged to be certain that a proof is correct is to have a machine check it<\/a>. But it did not come for free. Hales and Ferguson announced the Kepler proof in 1998 but the machine-checked proof arrived in 2014. Hales, in a guest post on Terrence Tao’s blog<\/a>, shared his estimate of the human effort that went it:<\/p>\n\n\n\n the formal proof of the Kepler conjecture on sphere packings in three dimensions took about 20 human work-years.<\/p>\n<\/blockquote>\n\n\n\n Early September, OpenAI announced what it called a solution<\/a> to one of the seven Millennium Prize problems, the Navier-Stokes. It shared that the agents took about 88 hours to arrive at it. The verification that it was valid using Lean formalization took an additional 17 hours and an AI model, GPT-6 Astra, did it. Lean is a computer program and a language that allows mathematicians to verify and guarantee that a proof has no errors, akin to a spell-checker that can help a writer make sure there are no spelling errors. <\/p>\n\n\n\n And on October 6th, OpenAI shared 722 more manuscripts in a single release<\/a>. On average, it reported that each result used three hours<\/a> of ChatGPT Pro compute. <\/p>\n\n\n\n Doing got cheap<\/a>, and now checking did too. What happens when both are cheap, and who pays for it?<\/p>\n\n\n\n Others have already made the case that what it means to be a correct proof has diverged from what it means to be understandable. In the words of De Toffoli and Duede<\/a>,<\/p>\n\n\n\n We can end up with formal proofs that float free from any intelligible proof.<\/p>\n<\/blockquote>\n\n\n\n Sanderson captured the essence<\/a> when he wrote<\/p>\n\n\n\n … every AI-generated proof is born an unsolved exposition problem.<\/p>\n<\/blockquote>\n\n\n\n Tao summed it up in a lecture at Caltech that we are entering a new era<\/a><\/p>\n\n\n\n we are now entering an era of proof abundance in mathematics.<\/p>\n<\/blockquote>\n\n\n\n In my earlier post on the topic, I wrote that the machine check does not remove trust from the picture but moves it. In this post, I want to address where it moved to.<\/p>\n\n\n\n OpenAI has committed to preserve the public release history. There are 719 manuscripts across 372 families, resulting from approximately 4000 problems that were posed to the model. We have to be careful to not read this as a success rate. OpenAI has not shared how the problems were chosen or what happened to the rest but said selection was by “requiring an appropriate level of significance.” 300 of them, about 42%, have been shared with a machine check and OpenAI warns that “some of the unformalized results could have issues.” A spokesperson told Retraction Watch<\/a> that \u201croughly 50% of the results were released unconfirmed.\u201d<\/p>\n\n\n\n Some had issues. The log for October 7 records three papers withdrawn. One contained \u201ca sign error\u201d that \u201cinvalidates a stabilization-trace cancellation argument and the construction used by two dependent papers.\u201d The company found it. \u201cA spokesperson for OpenAI told us the company identified the errors during an audit,\u201d Retraction Watch reported. The same day, fourteen more manuscripts were revised, with \u201cproof repairs, corrected statements, clearer hypotheses and dependencies,\u201d and thirteen more were updated to cite the revised versions. Thirty manuscripts changed in a day.<\/p>\n\n\n\n The gap between claimed and accepted is older than this release. MIT FutureTech tracks<\/a> the 457 problems on Wikipedia\u2019s list of unsolved problems as it stood in January 2024. By late September, 30 had been resolved, and \u201conly 9 have been formally accepted; the rest are claimed but not yet verified.\u201d The author adds that AI agents compiled the statuses, and that \u201cthe individual proofs have not been hand-reviewed by any expert mathematicians.\u201d<\/p>\n\n\n\n In the book<\/a> I use mathematics as the cleanest case for letting machines attempt everything. Three conditions make that safe. You can say in advance what success is. You can detect failure promptly. You can reverse a failure before it spreads. In mathematics, I wrote, \u201cverification is cheap and failure is free.\u201d October tested each condition in the one field where they hold best.<\/p>\n\n\n\n A theorem statement looks like the sharpest success criterion there is. In July I named two places the trust goes when a machine does the checking: you have to trust \u201cthat the formal statement fed to the checker is the statement anyone cared about, and that the checker itself is sound.\u201d October showed a third.<\/p>\n\n\n\n First, the statement. OpenAI describes its Navier-Stokes result this way: \u201cThe fluid has a smooth force applied to it.\u201d Two specialists in singularity formation, Diego C\u00f3rdoba and Luis Mart\u00ednez-Zoroa, note<\/a> that the claim, if verified, would meet one of the alternatives in the prize statement, and that it differs from blow-up without forcing. Hales states the rule: <\/p>\n\n\n\n a proof in Lean should not be accepted until a human audit is performed to ensure statement fidelity.<\/p>\n<\/blockquote>\n\n\n\n He is fair to the other side. \u201cThis task is generally massively easier than checking the proof itself,\u201d and the Navier-Stokes formalization \u201chas already been confirmed by more than a dozen proof-checkers.\u201d Easier per result still means a specialist per result. There are 300 of them.<\/p>\n\n\n\n Second, the translation. On the day of the release, Alexander Bastounis, Fabian Circelli and Anders Hansen posted a paper<\/a> comparing OpenAI\u2019s Lean proof of the Navier-Stokes result with its written proof. Their finding: <\/p>\n\n\n\n the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations.<\/p>\n<\/blockquote>\n\n\n\n NL is natural language. In one estimate, the written proof needs four derivatives of a quantity and the Lean version assumes five, which makes the Lean statement weaker. The authors take no position on whether the written proof is correct. Their point is about the method. A model translates the paper into Lean and revises until Lean accepts. Lean then confirms that the Lean proof establishes the Lean statement. Whether either one matches the paper is a separate question, and Lean does not ask it.<\/p>\n\n\n\n Third, the checker. Hales reports that Lean\u2019s kernel had soundness bugs this summer. \u201cOne Lean bug led to an illicit disproof of the Collatz conjecture.\u201d He learned of another when \u201cit produced a short illicit proof of the Kepler conjecture in Lean.\u201d That is the theorem from my opening paragraph, proved falsely in a few lines. The bugs were repaired. His conclusion stands: \u201cwe absolutely cannot put blind trust in systems such as Lean.\u201d<\/p>\n\n\n\n The three have something in common. Whatever makes the proof can keep adjusting until the check passes. Tao\u2019s lecture asks the same question of a clinical trial: <\/p>\n\n\n\n Could the AI solution be somehow misaligned by exploiting a weakness in the trial process or its math models?<\/p>\n<\/blockquote>\n\n\n\n I think this adds a fourth condition to the three in the book. The check has to be independent of the maker. I take that up in this week\u2019s newsletter, because it amends what I wrote in July about medicine.<\/p>\n\n\n\n Lean detects a broken proof at once, within the limits above, for the 42 percent it covers. That share had not moved a week later. Six formalizations were added on October 7, and the log has no later entry as I write.<\/p>\n\n\n\n For the rest, detection means a specialist reading a paper. The one failure we know of was caught by the producer\u2019s own audit. Outside readers describe their capacity plainly. Asaf Karagila, a set theorist, called<\/a> the release \u201cthe equivalent of a Denial of Service\u201d and declined to read the paper in his own field. Bryna Kra, a former president of the American Mathematical Society, told the New York Times: \u201cPeer review is gone in this process.\u201d On the one result she most wanted to read: \u201cThe writing, however, makes it impossible to understand.\u201d Scott Aaronson\u2019s summary<\/a>, the day after the release: \u201cit also appears that no human has understood just about any of these proofs yet.\u201d<\/p>\n\n\n\n We see only the errors that were found. The MIT post asks how many problems the models failed on. The same question applies to checking. I found no public count of how many of the 719 manuscripts a person has read.<\/p>\n\n\n\n The README says: \u201cSome outputs build upon earlier results produced by the models.\u201d The sign error shows what that means. One mistake took three papers, because two had been built on the first before it was checked. I wrote about this shape in Nothing to Declare<\/a>: outputs consumed by other systems without a contract, and nobody owning the pair.<\/p>\n\n\n\n A failed attempt costs tokens and spreads nothing. An unchecked success gets cited. This time the withdrawal worked, because a public log existed to record it.<\/p>\n\n\n\n Tao raised a harder case the same day<\/a>. Some of this cannot be reversed at all. \u201cA problem that has been \u2018solved\u2019 cannot be somehow reverted to become \u2018unsolved\u2019,\u201d he wrote, and knowing a solution exists \u201ccontaminates\u201d the search for other routes that might teach more.<\/p>\n\n\n\n That leaves understanding. Amit Sahai, a computer scientist, described<\/a> the unit of work: research groups \u201ceach spending a term or a year trying to understand an extraordinary set of ideas produced by an AI system.\u201d <\/p>\n\n\n\n Models will help write the explanations, and the MIT post expects the human edge there to be \u201cshort lived.\u201d I grant that. Writing an explanation gets cheap. Absorbing one does not. Sahai again: \u201cDepth of understanding needs time and a pace of life that humans can sustain.\u201d<\/p>\n\n\n\n Tao describes<\/a> what used to pay this bill. A breakthrough brought talks, workshops and newcomers, and through that activity proofs \u201cbecome digested, streamlined, placed in context.\u201d For machine results he reports<\/a> the opposite: \u201cMany fewer seminars, workshops, collaborations, or other activities are being generated from these results compared to traditional breakthroughs.\u201d Solutions, he says, are being \u201charvested at large scale in an unsustainable fashion.\u201d Kra says the same from the other side. \u201cBy releasing this trove of material in this manner, the companies are in the process of destroying the ecosystem that made it possible for this work.\u201d A mathematician who uses the tools, she adds, \u201crisks giving their ideas away.\u201d<\/p>\n\n\n\n That is the vocabulary of a commons. I have used it<\/a> for enterprises: \u201cThe deploying team enjoys the benefit and the enterprise absorbs the cost. That is the textbook definition of an externality.\u201d The mathematicians advising OpenAI use the same word. Their guidelines<\/a> warn of \u201csubstantial negative externalities that this practice inflicts on the mathematical community.\u201d<\/p>\n\n\n\n Two ways of paying the bill are now apparent. The first is to release everything and let the field digest it. Aaronson calls the resulting work \u201cthankless, barely-credited, competitive, and unfun.\u201d The second is for the producer to pay experts to digest a result before release. Aaronson reports that Anthropic gave Virginia Williams and Josh Alman a model\u2019s result to write up and announce, and compensated them. He names the cost of that route too. It \u201cputs a private company in the position of picking and choosing which human mathematicians\u201d speak for the machine.<\/p>\n\n\n\n The advisory group\u2019s answer is that the producer pays and the community leads. Labs \u201cmust take responsibility for ensuring that human understanding will follow\u201d and \u201cshould provide significant support, including funding,\u201d while understanding \u201cmust remain organic and community led.\u201d The group also asks for disclosure: \u201chow many other problems of comparable difficulty the models tried and failed to solve, as well as how the problems were chosen.\u201d OpenAI supplied part of this. The formalization status, the change log, the compute, the count of problems posed, and a promise to fund \u201cworkshops, conferences, and special programs\u201d with no amount stated. The README is silent on failures and on selection.<\/p>\n\n\n\n Mathematics is as well equipped for machine output as any field. It has a proof checker, specialists, an advisory group, and a habit of labeling what has been checked. In this release it also had a public log. With all of that, here is the record so far. Under half of the output was machine-checked a day after release. A paper disputes what the September check certified. One error traveled through three papers. Funding for understanding is promised and unspecified.<\/p>\n\n\n\n\n
What is already settled<\/h2>\n\n\n\n
\n
\n
\n
The accounting<\/h2>\n\n\n\n
What the cheap check bought<\/h2>\n\n\n\n
Saying what success is<\/h3>\n\n\n\n
\n
\n
\n
Detecting failure promptly<\/h3>\n\n\n\n
Reversing a failure before it spreads<\/h3>\n\n\n\n
The bill<\/h2>\n\n\n\n
The best case<\/h2>\n\n\n\n