You may be overconfident here. The NL paper may be properly stating the Navier Stokes problem, and the Lean code may not be.
Here's from the paper--
3.1. When the NL paper declares stronger statements than what Lean proves
We commence with an example that complements those in §2. In the following example the AI autoformalisation results in a different Lean proof of a weaker statement.
None of the examples are of the NS lean statement. The validity of the latter is not under question ( in this paper ). Please note the distinction between “statement of NS” and “statement of lemmas used in the NL proof of NS”.
Here's from the paper--
3.1. When the NL paper declares stronger statements than what Lean proves
We commence with an example that complements those in §2. In the following example the AI autoformalisation results in a different Lean proof of a weaker statement.