Comment by _flux

Actually, as an earlier commenter noticed, it seems that the proof was done in natural language, and only then translated to Lean, as https://openai.com/index/navier-stokes-solution/ says:

> The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT‑6 Astra.

So it suggests that the formalization/verification step may have fixed some issues in the natural language proof, and either such differences were never noticed or the corrections weren't ported back to the NLP.