Comment by ndriscoll

I'm pretty sure Mathlib has had enough human authored definitions to formalize the basic calculus necessary to state Navier-Stokes for quite some time? Some other problems admittedly need quite a bit of machinery built up to even try to say what the question is, but every undergrad learns multiple approaches to formally define everything necessary to write down a PDE.