I will give an overview of the state of formalising differential equations in mathlib: while results about PDEs themselves are still in its infancy, the ODE side looks much better, and many prequisites about PDEs are coming into place right now. I will comment on some challenges for formalisation in analysis and what we can do to improve the situation. As a concrete example, I will discuss the formalisation of Sobolev spaces (using classical distributions and weak derivatives); this is ongoing work with Filippo Nuccio and Floris van Doorn.