That could be that these examples are lemmas, but in the introduction the authors conclude,

"In all cases the correctness of the formal proof does not say anything about the correctness of the NL proof."

The Clay Mathematics Institute has not yet accepted the proof as it takes a while to review.

"The Clay Mathematics Institute is dedicated to furthering the beauty, power and universality of mathematical thought. Curating the Millennium Prize Problems is one of the most important ways in which it pursues this goal. The rules governing the prizes describe the process for evaluating what has been achieved and for assigning credit. The process is deliberately unhurried, but we will provide updates."

https://www.claymath.org/news/navier-stokes-announcement/

We can see therefore that we don't know if the OpenAI program wrote the NL statement or proof correctly. Or if maybe it needs work. Or if maybe it has significant errors.

We also don't know if Astra properly wrote the initial statement of Navier-Stokes correctly in Lean.