Comment by balaclava9

My understanding is that the statements in the Lean proof might not actually correspond to the Navier-Stokes problem. And that requires mathematical insight to be able to verify, which could take quite a while.