AI, academia and a millennium problem

Mathematical academia is usually a peaceful place, where controversy happens in the span of months, or longer. Debates take place one conference at a time. The last year has not been so. The use of LLMs in research has both sped up the pace of progress but also opened up many questions, including what it means to research mathematics and what is its goal (Leiden declaration).

The latest, most dramatic and highest stakes of this program has developed over mere hours. Little more than 24 hours ago, Tristan Buckmaster published a post on Mastodon comprising of three papers and a statement. The papers show a way towards proving the Navier-Stokes millennium price. I am not an expert in the field and I have had absolutely not enough time to even look at it, but my understanding is that proving a blow up in finite time of a forced solution of NS would be a counter-example of the millenium problem as stated. Buckmaster was a step behind, proving it for two other “stepping stone” equations (Euler 3D and Bussinesq). Not only this would be incredible news in and of itself, but there is way more to it. Buckmaster states that he is forced to publish ahead of his intended schedule because the result could be snatched from under him. Indeed, in his statement, he explains how the papers are a result of a collaboration with Levent Alpöge, an Anthropic employee, and have been developed with “significant help” from a variety of LLMs [edit: including OpenAI’s Codex]. Recently, OpenAI contacted Buckmaster following rumors that he had a proof. OpenAI stated they had a full proof, that they reached to with “minimal human input” and that happened to follow exactly Buckmaster’s technique. After prodding, the limited human input seemed to be false. OpenAI then admitted that a full team had been working on the matter and that their team started working on it after Buckmaster had his own main result. OpenAI, according to Buckmaster, refused to answer if the LLM they used had been trained on Buckmaster’s proof itself. They seem to have proposed to either publish “together” but excluding Alpöge in two different ways. Taking directly from Buckmaster’s statement because wording is of the essence: “Two proposals were offered to me [Buckmaster]. The first was that we post our Euler result, and that OpenAI post its Navier-Stokes result the next day. The second was that, after posting Euler, I alone write a paper presenting the Navier-Stokes result, acknowledging that an internal OpenAI model had resolved it. Sebastien twice asserted that he wanted Levent removed from authorship, and said it would all be simple if only it were not the case that, and it was so annoying that, Levent works at Anthropic. It was also said that if OpenAI posted after us, they would say that we deserved the Clay Prize, and that we were the “closest humans to the problem”. I declined both offers.”

After declining and stating he would go public, it seems OpenAI asked “Why would you ruin your career?”

He then went public with both the proofs “as is”, and the statement. By the end of day, OpenAI made their announcement, with a declaration on their LLM based, Lean certified proof of Navier Stokes: post in X .