Comment by JohnKemeny

It's highly non-trivial to confirm that the theorems written in Lean are actually the same as the Navier–Stokes (non-)theorem.