What the OpenAI Math Controversy Means for Enterprise AI Governance

I spent part of this week on two OpenAI stories.

On September 8, OpenAI said an internal model proved the three-dimensional Navier-Stokes equations can blow up in finite time. That's one of the six unsolved Millennium Prize Problems. If you don't believe them, clone the GitHub repo, run lake build, and let Lean check every step.

Five days earlier, NYU's Tristan Buckmaster asked OpenAI something else. He and Levent Alpöge had spent a year putting drafts into Codex. Had the model trained on that work? OpenAI's public position: while unlikely, it "cannot rule out that de-identified data derived from their usage of our products helped improve our models."

I use these tools extensively across engineering, marketing, and business work. The Lean repo is something I can copy. Most companies I talk to are running on a vendor statement they cannot check.

Did OpenAI solve Navier-Stokes?

About 10,000 agents, September 1 to September 5, roughly 88 hours. 2.7 million messages between them. About 130 billion output tokens. Chief Research Officer Mark Chen put the cost in the millions of dollars, roughly a thousand times earlier mathematical experiments.

The model was an unreleased internal system. OpenAI says training of the internal model began August 28. That came shortly after a two-week pause in reinforcement-learning training on its latest deployment-bound models following the Hugging Face security incident. Chief Scientist Jakub Pachocki: "This is not the result of some long-going effort at OpenAI to solve the Millennium Prize problem. This is an evaluation of a system for general purpose intelligence." GPT-6 Astra, the public flagship, formalized the result in Lean 4 afterward. That took another 17 hours.

What they proved is narrower than the headline. The Clay Institute's official statement lists four alternatives. OpenAI's repo claims two of them, (C) and (D): there exist smooth initial data and a smooth applied force for which no global smooth solution exists, on all of space with bounded energy and on the periodic torus. The force is the part mathematicians are arguing about. The written problem allows it. Many mathematicians had the unforced case in mind, and Quanta reported that some in the field view the forced route as a loophole. OpenAI declined the prize. Clay president Martin Bridson said the evaluation would be "deliberately unhurried" and "absolutely rigorous." The institute still lists the problem as open.

The smooth-forcing direction had important prior work. Diego Córdoba and Luis Martínez-Zoroa opened it in 2023 with a program that achieved blow-up with rough forcing. Buckmaster and Alpöge — Alpöge is a mathematician at Anthropic, working on this independently — spent nearly a year pushing that program from rough forcing to smooth forcing with Codex and Claude. On August 15 they got the Euler equations, the frictionless cousin of Navier-Stokes, to blow up. On August 22 they had it verified in Lean. Buckmaster's description of the first LLM-generated proof Alpöge sent him: "the most horrendous I have ever read." They spent weeks rewriting it into something humans could follow, and posted at midnight on September 7.

OpenAI's Sébastien Bubeck says the trigger was social media: "we saw rumors on Twitter that Anthropic might have solved two Millennium Prize problems. So we thought to ourselves: 'We have such a strong model. Why don't we try to solve also a Millennium Prize problem?'" They tried all six, settled on Navier-Stokes, and went through unforced Euler first, nearly 100 agents over about 50 hours, then on the order of 10,000 concurrent agents on the full problem. OpenAI says its researchers and agents did not see Buckmaster and Alpöge's work before it was public, that no specific user data was accessed to solve the problem, and that the proofs differ significantly — including forced versus unforced Euler. Buckmaster: "It is not the direction one arrives at in a few days by giving a model the problem statement."

How to verify OpenAI's Navier-Stokes proof

This is the part I would copy.

Lean is a proof assistant. A small kernel checks every inference against the definitions and theorems it depends on. The repo pins Lean 4.34.0-rc2 and Mathlib. It also ships Comparator challenges, so a second, independent checker can re-verify the exported proof. The problem statement it checks against was adapted from DeepMind's Formal Conjectures formalization, so you aren't stuck with OpenAI's wording. If you think their Lean build is lying, you can route around it.

Lean will not tell you whether the theorem it checked is the theorem everyone meant. Quanta put that leftover job cleanly: the verification "that must still be done by humans is to guarantee that the statement being shown to be true in Lean is logically equivalent to what mathematicians set out to prove." Read the formal statement. Compare it against the Clay PDF. Argue about the forcing term. Days of expert work, in public, on a fixed text.

Terence Tao has a serious objection about a "decoupling between getting answers and getting understanding." That's a real complaint about how math gets done. The Lean kernel still either accepts the proof or it doesn't.

Did OpenAI train on Buckmaster's Codex drafts?

Buckmaster's four-page statement starts September 3, when rumors of an OpenAI result began circulating. His opening email included a line I keep coming back to: "this is not an institutional effort. It is a strictly personal collaboration between the two of us, and there is no formal agreement behind it. I pay for the tools my group uses out of my own research funds, including footing a large bill to OpenAI."

Then the question: "I asked whether the model had been trained on, or had access to, our sessions in Codex, into which we had been putting all our drafts for the whole of this project." On agents, he was told the model "did not look up user data." On training: "I asked again, about training, and I did not get an answer." OpenAI's later public position: "While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models." Bubeck, separately: "We did not use their prompts or proofs to prompt our models or direct our agents."

Then it got uglier. Buckmaster says OpenAI proposed that he alone write a paper presenting OpenAI's Navier-Stokes result and says Bubeck twice objected to Alpöge's authorship because Alpöge works at Anthropic. Bubeck disputes that characterization: he says he never sought to remove Alpöge from authorship of the pair's own work, and that the discussion concerned Buckmaster potentially leading a rewrite of OpenAI's separate proof. Buckmaster says that when he threatened to go public, Bubeck replied, "Why would you ruin your career?" Bubeck has apologized for that remark as an "extremely poor choice of words." Buckmaster himself is careful: "I have not seen OpenAI's proof. I do not know what their model did. I am not accusing anyone of anything."

There is no lake build for a training corpus. Buckmaster can't inspect it. Outsiders cannot independently verify the answer from what is currently public. On personal Free, Plus, and Pro workspaces, data sharing for model improvement is enabled by default unless you opt out. Codex has separate controls for full-environment training. OpenAI says inputs and outputs from ChatGPT Business, Enterprise, and its API are not used for model training by default. Whether any given year of drafts ended up in a corpus depends on which account, which toggle, and which date — and that configuration is not something an outsider can see.

What "we cannot rule out" means for your company

If you run technology for a company, you're looking at the same verification problem at scale. Contract drafts, source, the roadmap, the deal the sales team is working. All of it moving through a lab's product every day. If your organization cannot answer Buckmaster's question from its contract, workspace configuration, and system architecture, you have a governance gap. I've read a lot of AI policies where "we trust the vendor" or "we use the safe one" is standing where a control should be.

I've been in that chair. I've written twice this summer about not getting married to a model, once when a Commerce directive switched Fable off mid-evaluation and once when a watermark I never asked for shipped worldwide. This week is about what you put in, and whether anyone outside the vendor can check where it went.

At Zenpo we run on ChatGPT Business and Claude Team. The reason is specific: OpenAI does not use ChatGPT Business inputs or outputs for model training by default, and Anthropic says the same for inputs and outputs from its commercial products. I don't want our policy to depend on every user remembering a consumer-account toggle. When AI use is appropriate, proprietary client or company work goes in a managed business workspace, not a personal workspace.

How to keep company data out of model training

Buckmaster and Alpöge used Codex and Claude for a year and came out with a Lean-verified Euler blowup and a route to Navier-Stokes. That's the part to copy. Nothing in this story argues for using the tools less. Replace each place you're trusting with something you can check.

Make the artifact carry its own proof. Lean is the extreme case. You already have the ordinary versions: tests the model didn't write, type checks, schema validation, migration dry runs, a diff of generated contract language against your own template. When the check is independent of the generator, a lying model still has to pass the tests. Skipping the verification layer is the failure I keep seeing under new names, whether the generator is a junior developer or 10,000 agents.

For what you put in, use commercial terms that explicitly exclude customer content from model training by default. OpenAI does this for ChatGPT Business, Enterprise, and API usage; Anthropic does it for its commercial products. Zero Data Retention is a separate OpenAI control available to eligible API customers; ChatGPT Business is not ZDR by default. An actual inventory of which account each person is logged into. A Plus seat with the toggle off is a setting someone can flip, on a plan the vendor can change. Verify it the way you'd verify any other access control, on a schedule, against what people are actually doing rather than what the policy says they do.

Keep provenance somewhere the vendor doesn't own. A timestamped public release helped establish when Buckmaster and Alpöge's work became public. Signed commits, dated preprints, and internal timestamped records serve the same purpose for companies. You want that record before you need it.

And ask the question at onboarding. Buckmaster asked on September 3, after nearly a year of using Codex on the project. Put "can you train on this, and how would we know" in the vendor questionnaire next to the SOC 2 request. If a vendor cannot give you a contractually clear answer before sensitive work goes in, change the account, the configuration, or the architecture.

Tao warned about turning historically productive problems into benchmark moments. OpenAI's own account shows how quickly that can now happen: a rumor was enough to trigger a multimillion-dollar effort. That raises the same governance concern for any company whose proprietary plans sit inside a vendor's product. The capability exists. Put the no-training term in writing, then back it with account controls, data classification, an inventory you actually audit, and an architecture that keeps sensitive work out of personal workspaces.

Put the question in the questionnaire this week, while the drafts are still on your side of the wire.

Did OpenAI solve the Navier-Stokes Millennium Prize Problem?

OpenAI claims to have proved alternatives (C) and (D) of the Clay statement: smooth initial data plus a smooth applied force with no global smooth solution. The result is formally checked in Lean. OpenAI declined the prize, the Clay Institute has not accepted the result, and mathematicians dispute whether the forced case is what the problem meant.

Can anyone verify OpenAI's Navier-Stokes proof?

Yes. The Lean 4 formalization is public on GitHub and builds with Mathlib, and the repo includes Comparator challenges for independent re-checking. Humans still have to confirm the formal statement matches the Clay problem as written.

Did OpenAI train on Buckmaster and Alpöge's Codex sessions?

Outsiders cannot independently verify. OpenAI says neither its researchers nor its agents saw their work before it was public, and that while unlikely, it "cannot rule out" de-identified usage data improved its models. No independent public verification of those data-provenance claims is currently available.

Does an enterprise AI plan protect our data from model training?

OpenAI says ChatGPT Business, Enterprise, and API data is not used for training by default. Anthropic says inputs and outputs from its commercial products are likewise not used for training by default. Personal-workspace rules differ by provider, so the control is knowing which workspace people are actually using and what terms govern it.