mc2022-Lean Source code for a class on Lean at Mathcamp 2022 Download this project using leanproject get awainverse/mc2022-Lean To generate the html pages, you'll need pip and leanproject. Run make html examples latexpdf in the src folder.