OpenAI says AI agents resolved Navier-Stokes problem; formal review still ahead

According to OpenAI's account, as reported by Quanta Magazine, the agents worked for about 88 hours, after which a separate model spent 17 hours translating the argument into the Lean proof language. OpenAI researcher Sébastien Bubeck estimated the computing cost at several million dollars. The claimed result is a finite-time blowup, in which a flow that starts out smooth develops a singularity.

Quanta reported that the Lean check gives mathematicians confidence the argument is sound, but that people must still confirm the formal statement matches the problem as mathematicians posed it. The Clay Mathematics Institute, which offers $1 million for a solution, said on Sept. 11, without naming OpenAI, that the problem has apparently been settled and that evaluation and credit will follow its prize rules without haste.

Credit is disputed. Tristan Buckmaster of New York University and Levent Alpöge, who obtained a Lean-verified proof concerning the related Euler equations in August, have suggested OpenAI's agents may have benefited from their use of OpenAI's models. OpenAI has said its researchers and agents did not see the pair's work before it became public. Princeton mathematician Charles Fefferman welcomed the result.