Terence Tao Criticises OpenAI’s 719 AI Math Proofs: “Proof Indigestion”

October 9 (IT Home) — OpenAI published 719 AI-generated mathematical solutions in October, covering 372 families of mathematical results and hundreds of open research problems. After publication, however, it was pointed out that the release does not fully meet the standards set out by the Advisory Group on Mathematics and Artificial Intelligence (AGMAI).

IT Home previously reported that OpenAI first published a total of 722 AI-generated mathematics manuscripts on GitHub on 6 October, covering 372 result families and a number of open research problems. On 7 October it withdrew three of them because of a notation error and its knock-on effects, leaving 719 in the public catalogue.

OpenAI says it consulted AGMAI — convened by the Institute for Advanced Study in Princeton — before publication and took its public recommendations into account. Publicly available information suggests, however, that the release does not fully meet the group’s standards.

AGMAI had recommended that frontier AI labs stop testing difficult mathematics problems on proprietary models that outsiders cannot access, and required disclosure of the model name, prompts, reasoning chains, time taken and compute costs. OpenAI nonetheless used proprietary models, and only 10 manuscripts include the model’s reasoning chain.

On human comprehensibility, the advisory group stressed that AI-generated proofs should be easy for mathematicians to review and learn from. According to reports, however, about 42% of the proofs OpenAI published have not been formalised, and no machine-readable metadata linking the natural-language proof to a formalised artefact was provided.

AGMAI also stated that its advisory role does not constitute an endorsement of OpenAI obtaining or publishing these results, and that it is ultimately up to the mathematical community to assess whether the recommendations have been adequately followed. The episode has reignited debate about transparency, formal verification, peer review and the autonomy of academic research in AI-generated mathematics.

On 7 October, Terence Tao posted on mathstodon saying that he is not opposed to AI doing mathematics — he has even been an active user of AI-assisted research — but that he strongly opposes making “using AI to quickly crack famous problems” a primary goal or a product demonstration. He argues that it damages the mechanisms of understanding, teaching, collaboration and open exploration on which the mathematical community depends.

Tao points out that in traditional mathematics, a breakthrough on a long-standing conjecture is not just “getting the answer”: the author gives talks, attends seminars and exchanges ideas with peers; the proof is then simplified, explained and incorporated into textbooks, and it spawns follow-up questions, collaborators and new lines of research.

With the current approach of companies such as OpenAI, by contrast, a prompter drives the AI to solve problems autonomously; once the goal is “solved,” the subsequent understanding, reporting, peer discussion and field-building rarely happen. Tao argues that the publishers may not even be able to explain the AI’s output, answer questions or engage with the field.

He calls this situation “proof indigestion” in mathematics: AI can generate propositions, proofs and counterexamples at high speed, but humans cannot verify, understand, write up, teach and absorb them in time, leaving a large number of “proofs no one can digest.”

He is especially concerned that OpenAI treats Millennium Prize problems such as the Navier–Stokes equations as benchmarks of model capability. In his view, this turns “how many problems were solved, and how quickly” into a measure of “understanding and insight” — but speed and quantity do not in themselves equal mathematical understanding.

Tao stresses that once a problem has been publicly “solved,” it can hardly be restored to an “unsolved” state. Even if people later want to look for different routes and distil new methods from it, merely knowing that an answer exists will “contaminate” that process of exploration.

He therefore criticises this as unsustainable large-scale “harvesting”: treating open problems as a resource to be consumed in bulk, which in the end will leave the whole field of mathematics less fertile than it would be under traditional ways of doing research.

IT Home notes: Terence Tao is one of the most renowned mathematicians of our time, a professor of mathematics at the University of California, Los Angeles (UCLA), and a 2006 Fields Medal winner; he is often called “the Mozart of mathematics.”