On September 8, 2026, OpenAI shared a claimed resolution of the Navier–Stokes Millennium Prize Problem.

This is not the first claim of this kind. In December 2025, a (smaller-scale attempt) by a former DeepMind engineer was quickly dismissed.

Yet this time, there has been a paucity of publicly voiced doubts about the correctness of the generated proof (though there have been significant concerns about OpenAI's handling of attribution).

One reason for this lack of skepticism is the accompanying Lean formalization.

This, in turn, raises two important questions:

(1) Why can we trust LLM-generated Lean certificates?

(2) How can we verify that the Lean statement is a faithful translation of the Navier—Stokes problem?

These questions are not currently solved, but I will offer practical partial answers to both, as they connect to ongoing autoformalization efforts in mathematical logic.

No prior knowledge of Lean or mathematical logic will be assumed.

Part of this talk is based on joint work with Aaron Crighton, Deirdre Haskell, John Nicholson, and Jonas van der Schaaf.