> They are claiming that we do not know if Astra formalized all the elements of the Navier-Stokes proof in Lean correctly. This has nothing to do with whether the lean proof certifies (the real) NS.
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…
Curious to hear more about the team/problem. (I’m a mathematician in the middle of trying to convince companies that I’m useful)
> They are claiming that we do not know if Astra formalized all the elements of the Navier-Stokes proof in Lean correctly. This has nothing to do with whether the lean proof certifies (the real) NS.
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…
Curious to hear more about the team/problem. (I’m a mathematician in the middle of trying to convince companies that I’m useful)