OpenAI claims AI-assisted Navier-Stokes proof but cannot rule out training on private drafts

OpenAI has published a formal write-up claiming that an internal AI system produced an analytical proof that three-dimensional incompressible Navier-Stokes equations can develop a finite-time singularity, a core Millennium Prize problem, with GPT-6 Astra completing the Lean formalization used for verification. On the same day, September 8, 2026, the company issued a statement conceding it cannot rule out that de-identified data derived from a competing mathematician's private sessions with its own products helped improve its models.

The claim

According to a dev.to report on OpenAI's write-up, the analytical proof came from an internal model that OpenAI describes as significantly more capable than GPT-6 Astra, which handled only the formalization step. Training of that internal model reportedly began around August 28, 2026. The proof effort ran with on the order of 10,000 concurrent agents for roughly 88 hours, after which GPT-6 Astra spent about 17 additional hours expressing the argument in Lean, a formal proof environment where computers check each logical step against defined rules.

The framing matters: this is not a claim that a publicly available model independently solved the problem, but a coordinated workflow in which one system generated the argument and another made it machine-checkable. OpenAI also says it intends to recognize priority for concurrent related work by Tristan Buckmaster of NYU and Levent Alpöge of Anthropic.

The rival work

A second dev.to report, drawing on Buckmaster's public statement, describes a parallel effort. Buckmaster and Alpöge spent most of a year on finite-time blowup for fluid equations, the family that includes the Navier-Stokes prize question, working with LLMs throughout: Claude, Codex, GPT-5.6 Sol and Astra. By August 15 they had blowup results for Boussinesq and 3D Euler, and by August 22 a proof verified in Lean.

Every draft went through Codex. In Buckmaster's words: "our sessions in Codex, into which we had been putting all our drafts for the whole of this project."

The call

The two dev.to reports differ on dates, one placing the first rumors on September 1 and the other on September 3, but the sequence that follows is consistent. Buckmaster emailed his contact at OpenAI and was soon on a call with Sébastien Bubeck, where he learned that an internal model had produced a roughly 100-page proof of finite-time blowup for forced Navier-Stokes, in the same smooth-forcing setup he and Alpöge had quietly chosen.

When he asked when the first prompt was sent, the eventual answer, per the report, was within the previous few days, after information about their work had already reached OpenAI. He then asked whether the model had been trained on, or had access to, their Codex sessions. He was told the model did not look up user data; pressed specifically on training, he received no answer.

His public account also included two proposals to coordinate release, a request that Alpöge be dropped from authorship because he works at Anthropic, and a line about not having to "be nice", which Bubeck has since called ill-chosen and retracted, according to the report. OpenAI's initial response called the allegations false and inflammatory.

The statement

OpenAI's September 8 statement, as quoted in the dev.to report, addresses the training question plainly: "While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models." The company separately asserts that no specific user data was accessed and that researchers and agents did not see the work, retrieval and visibility claims that leave the training question standing alongside that admission.

OpenAI also says the proofs differ significantly, and that the Euler results differ in being forced rather than unforced. As the report notes, nobody outside OpenAI, including Buckmaster, has yet seen the new proof, so independent mathematical judgment is still pending.

Why it matters

The claim and the controversy are inseparable. If the proof survives scrutiny, it would be a milestone in AI-assisted mathematics and a demonstration of a generate-then-verify pattern, one system proposing an argument and another formalizing it, that other high-stakes AI workflows could adopt. But a provenance question now attaches to the result: a year of unpublished work on a Millennium Prize problem sat inside a competitor's product, and the company cannot exclude that it shaped the model that then produced a concurrent result.

The report's broader point concerns defaults. Consumer Codex sessions are, by default, training data. "We cannot rule it out" may be the only answer OpenAI can honestly give, and it applies equally to every codebase, architecture decision and unpublished draft anyone has pasted into the product. Lean can verify a proof's logic; it cannot verify where the idea came from.