In case you are not aware, the actual theorem statement of N-S was never translated by an LLM, but was written independently by formal conjectures, as they say in the README [1].

A Lean proof has a much higher probability of being correct (in my opinion) than any published (either preprint or peer-reviewed) paper, yet no one before LLMs were walking around claiming every result published can't be trusted yet (without an actual reason).

We have seen one such instance of Lean bugs, which was found adversely against Lean (as in find bug then use this bug to prove Collatz, not just found when being asked to prove it).

It's also worth to note that the way N-S (and all the other proofs by OpenAI etc) have been found is first prove it in NL then translate to Lean. I.e. it would have to first believe it found a correct proof in NL, and then afterwards either accidentally or on purpose use a Lean kernel bug.

[1]: https://github.com/openai/NavierStokesAndEuler/blob/main/Com...

edit: Probably also worth to mention that the proof have been checked both by the Lean kernel and the independent nanoda kernel, so it would need to exploit bug(s) from both.