As a former stay at home Dad, I endorse the above message. Also, FYI, there is no trouble to fill the days with hard and rewarding tasks. (The question I would get from men at parties was always how I filled my time; with a 1 and 5 year old and a politician spouse!)
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.
Like the ascent to Mt. Hamilton (southern Bay Area). You can see the peak for like an hour but so much twisting back and forth, going mostly perpendicular to the max gradient. It is an old road and hence graded for mules to carry up telescopes.
No reason to think leaders are less persuadable than the proles. Lots of people can’t be reliably persuaded to do basic safety or health things or that the earth is round. And we have seen so many leaders throw billions away on obviously impossible projects, persuasive details from their teams be dammed.
Life is a bit easier when we see the conditions that lead to the undesirable outcomes, and so much harder when we aspire to perfect ourselves and use moral strength to over come our weaknesses. Like my mom always said of parenting, "Make it easy to be good." - works for self-management as well, and is much more relaxing and happy than constantly trying to grind or improve.
reply