OpenAI’s Navier–Stokes proof faces questions over method and formalization

OpenAI described the result as an analytical proof that a smooth fluid initially at rest can develop a singularity in finite time.[1] It said the fluid’s energy remains finite as the singularity forms.[1] OpenAI described the solution as a vortex that spirals inward and becomes increasingly elongated.[1] The proof uses a smooth external force while fluid velocity grows without bound, according to OpenAI.[1] The company said it was sharing both a written proof and a Lean formalization.[1]

OpenAI said the group involved on the order of 10,000 concurrent agents and reached its result about 88 hours after launch.[1] It said the agents used approximately 130 billion output tokens on the Navier–Stokes problem.[1] OpenAI described the internal model used for the work as significantly more capable than GPT-6 Astra.[1] Lean formalization and verification took an additional 17 hours using GPT-6 Astra, OpenAI said.[1]

OpenAI’s initial account said the proof followed an approach devised by Spanish mathematicians Diego Córdoba and Luis Martínez-Zoroa.[2] Scientific American reported that experts increasingly concluded the proof did not follow that program.[2] EPFL mathematician Gonzalo Cao-Labora said the approach differed from the Spanish program when examined in detail.[2] The report said the proof constructs its unnatural force in a distinct way, while some experts said a more modest squad followed the program.[2] It reported that the 10,000-agent group apparently took a different route.[2]

Researchers argued that the formalized Lean proof does not correspond to the natural-language proof of blow-up.[3] New Scientist reported that the written proof requires a value below m + 4, while the Lean proof requires it below m + 5; the latter bound is mathematically weaker because it allows more possible values.[4] Hansen said the researchers were not claiming either that the natural-language proof was wrong or that it was correct.[4] OpenAI told New Scientist it was aware of the mismatch and said it did not mean either proof was invalid.[4] OpenAI said it would correct errors found in the written proof and continue formalizing its 722 mathematics papers.[4]

New Scientist reported that researchers took about two weeks to find a true discrepancy, compared with the 88 hours OpenAI said its agents spent generating the proofs.[4] OpenAI said its researchers and agents had not seen work by Buckmaster and Alpöge before it was published, but it could not rule out that de-identified product-use data from them helped improve its models.[5] Tristan Buckmaster alleged that OpenAI researcher Sébastien Bubeck asked him, “Why would you ruin your career?”[5] Bubeck apologized for the question’s threatening sound and called it an extremely poor choice of words.[5] OpenAI said it did not intend to accept the Navier–Stokes prize for the result.[5]