Ааа, это прекрасно!

Поскольку в Навье-Стоксе я глубоко не разбираюсь, мой самый большой консёрн был по поводу того, как они получили Lean код, подтверждающий доказательство, и как быть уверенным, что этот код строго соответствует текстовому доказательству (а код был сгенерён уже после, отдельным процессом).

И вот, кажется, он не соответствует (но саму статью пока не читал):

https://arxiv.org/abs/2610.08144

To demonstrate the effect of this result we provide several examples of AI mistranslations of NL statements and proofs into Lean in practice, resulting in mismatches between NL proofs and their Lean `verifications'. These include OpenAI's announced Navier-Stokes proof. In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations.