AI-written proofs: OpenAI and Anthropic are paying for mathematicians to check them

One hundred sixty-six pages, written by a machine. On September 8, OpenAI claimed that one of its internal models had proved that the Navier-Stokes equations, which describe fluid flow, can "blow up": in certain rare cases, the fluid's velocity would become infinite at a point. It is one of the seven Millennium Prize Problems of the Clay Mathematics Institute, each carrying a $1 million prize. Five weeks later, the question is no longer just whether the proof is correct. It is also who will check it, and with what resources.

A first answer arrived on October 15. The Simons Foundation, a major American patron of mathematics, is launching a $15 million program in funding and resources with OpenAI and Anthropic. The goal: help researchers examine results obtained with AI, learn these new tools, and set common rules for their use.

Who pays, and who decides?

The foundation will manage the money and choose the recipients itself, partly through a call for proposals whose schedule has not yet been published. The program will fund workshops, conferences and specific programs. The two companies will also provide the supported researchers with access to their models and computing power, in mathematics and in the basic sciences. OpenAI announced a $5 million contribution; the foundation does not detail how the rest is split.

"The community must drive the discussions on how these tools are evaluated, adopted and used," says David Spergel, the foundation's president. A relevant detail: the Simons Foundation funded the development of Lean, the formal proof language that now makes it possible to mechanically verify proofs produced by an AI.

A disputed proof

The press release does not mention Navier-Stokes. Euronews, however, presents OpenAI's donation as an attempt to calm mathematicians' anger. The proof has set off a dispute over authorship. Mathematician Tristan Buckmaster (New York University) says OpenAI relied on unpublished work he was carrying out with Levent Alpöge, a researcher at Anthropic who was collaborating in a personal capacity. OpenAI denies this: according to Sébastien Bubeck, a mathematician at the company, his team used neither their prompts nor their proofs.

An organization, the Association for Human Mathematics, accuses OpenAI of plagiarism and of "total disregard for the norms of scientific research," according to Euronews. Other researchers are more nuanced. Gonzalo Cao-Labora, of EPFL, considers the two approaches different in their details, The Decoder reports. For Camillo De Lellis, of the Institute for Advanced Study, a definitive answer is probably impossible, because language models are black boxes.

Verified by the machine, not yet by humans

The proof is written in Lean, which checks every logical step and, according to OpenAI as quoted by Scientific American, almost guarantees its correctness. But a Lean text does not read like a mathematics paper. The Clay Mathematics Institute has been examining it since it was published, with no conclusion announced, according to The Decoder. The same site reports that the effort used about 10,000 instances of the model for about 88 hours, and that Noam Brown, an OpenAI researcher, acknowledges that nobody knows what each one contributed. In early October, OpenAI also published about 400 other AI-produced results, which part of the mathematics community received with skepticism.

The Simons program therefore raises a simple question: will mathematicians have the means to keep pace with the machines? The Clay Institute's verdict will be the first real test.