Contrarian scan

The strongest objections

❓ What would a skeptical specialist say first?

1. This is not the problem people meant.
(A) and (B) are unforced. Many lectures treat those as “the” Navier–Stokes problem. OpenAI solved the doors that allow a smooth force. Scientific American put this cleanly: Clay-as-written versus Clay-as-imagined. The objection fails as a rules argument and succeeds as a taste argument.

2. Applications will not move.
Silvester: mathematical nicety; CFD already good; wind tunnels largely obsolete. On a one-year engineering horizon this is the default.

3. The proof is unread.
A 165-page AI manuscript plus a large Lean development, public for hours, is not yet knowledge. Tao’s decoupling warning is the methodological version of this objection.

4. Clay has not spoken.
Rules: qualifying outlet, two years, general acceptance, CMI discretion. Bridson: unhurried and rigorous. OpenAI is not claiming the prize. Headlines that say “solved the Millennium problem” compress a process that took years for Poincaré.

5. Process contamination.
If Codex drafts or rumor-steering did the real choosing, then “an internal system produced a proof” is true in the way “a compiler produced a binary” is true. The objection does not automatically falsify Lean. It falsifies a myth of immaculate conception.

6. Crank physics.
Decades of claimed NS proofs exist. Some “allow feedback forces,” drop energy bounds, or confuse numerical blowup with theorems. OpenAI’s mapping to (C)/(D) with smooth compact force and bounded energy is why this claim is in a different class — if those conditions hold in the Lean statements.

7. Stale “still open” pages.
Sites last reviewed in July 2026 correctly said the prize was unclaimed then. They are not a 8 September referee report.

What would count as a real refutation

❓ What evidence should change the headline?

• Lean does not build, or the proved theorem is not Fefferman (C)/(D).
• Force fails smoothness or decay.
• Energy bound fails on \(\mathbb{R}^3\).
• A conceptual gap that Lean encoded (the kernel cannot save a wrong definition of “smooth force”).
• Clay later declining completeness.

Early named requests for scrutiny (including reports of comments by Gonzalo Cao-Labora) are watch items, not refutations.

Honest remainder

❓ What is still open even in OpenAI’s own frame?

Unforced 3D Navier–Stokes. Unforced 3D Euler is claimed by OpenAI as a separate theorem, itself awaiting the same social verification. Turbulence theory. A public model. A settled credit story. A prize.

If you came here asking “can the equations we fly planes with spontaneously explode with no outside push?”, the answer as of today is still: nobody has a Clay-grade yes or no.