How much lean code do you need to read to check if NAvier-Stokes was correctly formalized?

A tiny fraction compared to the proof, I'm guessing.

But the point is that you don't need to check the proof. But a lot of people seem to misunderstand what's happening and think you still need to check the Lean proof that AI outputs.