Comment by lanstin
3 hours ago
They do not. Maybe if they take Lean classes? Maybe starting this year they will but my youngest kid is on their like 5th math class in undergrad and hasn't had any lean at all. Not all undergrad math majors even take PDEs; applied maybe, unless you are doing applied discrete math (graphs, combinatorics).
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.
I'm not sure if calculus of constructions comes naturally to people who didn't have some experience with functional programming.