OpenAI says its AI solved Navier-Stokes. Codex users have another question

OpenAI published a claimed solution to the Navier-Stokes Millennium Prize problem on September 8. The company released an analytical writeup and a formal proof in Lean, saying an initially smooth fluid at rest can develop a singularity in finite time when a smooth external force is applied, while its energy stays bounded. OpenAI says this establishes both breakdown alternatives in the problem's official formulation: C on ℝ³ and D on the periodic torus ℝ³/ℤ³. Either result would settle the problem.

The Clay Mathematics Institute still lists the problem as unsolved. The proof needs outside scrutiny before it can be treated as an accepted resolution. Its formalization is public and mechanically checkable: the repository pins Lean 4.34.0-rc2 with Mathlib and Lake and includes a ComparatorChallenges directory for independent verification, but publication is not verification. OpenAI says it will not claim the prize.

The work began after rumors that two Millennium Prize problems had been resolved. The company reports that roughly 10,000 concurrent agents reached its Navier-Stokes result in 88 hours, using about 2.7 million messages and 130 billion output tokens. Lean formalization and verification with GPT-6 Astra took another 17 hours.

Another team had put its work into Codex

The rumors were connected to NYU mathematician Tristan Buckmaster and Levent Alpöge, a former Harvard Society of Fellows junior fellow who is now a member of Anthropic's technical staff. Their collaboration was personal, not an Anthropic research project.

In a statement published earlier that day, Buckmaster said the pair had made public three smooth-forcing, finite-time blowup results: for incompressible porous media, Boussinesq, and three-dimensional incompressible Euler. The arguments were formalized in Lean; a related hypo-dissipative Navier-Stokes result was awaiting verification.

The pair used several AI models, including Anthropic's Claude and OpenAI's Codex, especially GPT-5.6 Sol. Buckmaster said they had been putting drafts from the project into their Codex sessions.

Buckmaster also described asking OpenAI whether its internal model had been trained on, or had access to, those sessions. He says he was told the model did not look up user data, but did not receive an answer to the training question during that exchange.

OpenAI says neither its researchers nor agents saw the pair's work before publication and no specific user data was accessed to solve the problem. It cannot rule out, although it considers it unlikely, that de-identified data derived from their product usage helped improve its models.

That is not evidence that their drafts became Codex training data, influenced OpenAI's proof, or were copied. Buckmaster says he has not seen OpenAI's proof, does not know whether their data was used, and is not accusing anyone of doing so.

Buckmaster separately alleges pressure over the announcement and authorship. OpenAI scientist Sebastien Bubeck called the allegations false and inflammatory and disputed asking for Alpöge to be removed from his own work. Bubeck said Alpöge's use of internal Anthropic models on the Euler proof meant he did not regard Alpöge as an independent academic, and that he retracted his career remark during the call. OpenAI recognizes the pair's priority on forced Euler and considers the proofs significantly different.

According to OpenAI, it first tested all open Millennium problems; an unforced Euler result then led it to concentrate on Navier-Stokes. Terence Tao noted that the pair's methods could extend to Navier-Stokes in principle, and that enormous compute and AI assistance might overcome the technical details. An independent route is plausible, but that does not resolve provenance. OpenAI's inability to exclude an indirect contribution makes an ordinary product setting part of a research-credit dispute.

Data controls become part of the tool choice

OpenAI's current data policy says content from individual services may train its models unless the user opts out. Its Codex Help Center article says the controls apply to Codex content, including Computer Use screenshots.

In a reply posted later that day, OpenAI research chief Mark Chen denied that any person or agent looked at user data for this effort. He confirmed that feedback and de-identified data improve ChatGPT and Codex more broadly. OpenAI employee Ted Sanders, who said he was not on the proof team, added a narrower answer on HN: opted-out chats were not trained on; otherwise, he did not know whether signals from these chats were used and said identifying them would require the researchers' cooperation. Some readers saw a conflict between those statements. OpenAI's Data Controls FAQ says chats are not used to improve ChatGPT when training is off, while its Codex article says the same controls extend to Codex content.

Business, Enterprise, Edu, and API inputs and outputs are excluded by default. API organization owners can opt in, except Enterprise and Zero Data Retention customers. The researchers' product, workspace, and settings are unknown, so this episode does not show that OpenAI ignored an opt-out.

It does show why OpenAI data controls belong in a team's threat model. Developers hand coding assistants unreleased source code, architecture decisions, vulnerability findings, and product plans. De-identifying that material is not the same as excluding it from model improvement. A provider may also have the models, compute, and commercial incentive to work on the same problem later.

The Hacker News discussions about OpenAI's announcement and Buckmaster's statement center on training provenance, including the burden of proof and OpenAI's ability to trace training inputs. Reddit's technology and physics communities also debated the case. None of these discussions proves misconduct.

For personal accounts, the practical step is concrete: open Settings → Data Controls and turn off “Improve the model for everyone” before submitting sensitive material. Teams should also choose the business or API setup that matches their data policy. OpenAI's proof now faces mathematical review; its users are left with a harder product question about whether a provider can trace the provenance of a model result that lands close to their unpublished work.