For reference, a great intro to Lean for programmer-types without an academic maths background is Kevin Buzzard’s Natural Number Game: https://wwwf.imperial.ac.

For reference, a great intro to Lean for programmer-types without an academic maths background is Kevin Buzzard’s Natural Number Game: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam... Buzzard’s wider Xena project is formalizing a huge chunk of the undergraduate-level math curriculum into a “standard library” of math, written in Lean.