Not Lean specifically, but IMO it's pretty straightforward if you've done math and some programming (and at least my school required some programming).

Need to prove a forall statement? forall x, P(x) is the same as a function taking x and returning the proof that P(x) is true.

Need to prove an exists statement? Create the pair (x, h) that gives the actual x that proves the exists, along with a proof that it satisfies the property you claim.

Maybe the only weird thing is that there are types and sets, so sets are kind of automatically more of a "subset" of some type.

The actual Mathlib is more generic, but once you get a hang of writing definitions (as you do in intro proofs), I've found that you can pretty naturally translate whatever you'd have in your undergrad notes. And undergrad should cover defining integers, rationals, reals, relations, functions, sequences, limits, derivatives, integrals, etc. Even if they've never studied solving PDEs, they'd have to take multivariable calculus and know enough to be able to write one (assuming they take at least single variable analysis+linear algebra)?

The proofs can get involved and tedious with all of the extra bookkeeping, or techniques to try to reduce the bookkeeping (tactics, etc). But the definitions and statements are pretty much what you'd expect.

Lucky that it was enough in this case. The theorem had been written by formal conjectures before the proof https://github.com/openai/NavierStokesAndEuler/blob/main/Com...