This repository will house the code and slides for the Formal Proofs lectures at Monsoon Math Camp 2021.
You will need to install Lean+VS Code/Emacs for the best experience. The links below have OS-specific installation instructions and video walkthroughs.
If you don't want to try any of these, then Lean does work in a browser, but it may be slow and is not recommended for serious use.
After you install Lean and it's supporting tooling using the above links, open a terminal and type leanproject get kodyvajjha/lean-mmc2021 to clone this repository into your local computer. Next, open up the repository in either VS Code using the command code lean-mmc2021. You should now be ready to start proving!
This course will be more interactive than the other courses and you will have plenty of practice problems to work on at your own pace.
- Tactic cheatsheet: A list of most-used tactics.
- Matlib tactics: More advanced tactics.
- Your instructors will keep checking Discord in the
#formal-proof-generalchannel, through the week to offer help if you need it. - You are also encouraged to ask questions on the official Lean Zulip Chat. The Lean community is very beginner-friendly.
Here's a partial list of references you can follow:
- Theorem Proving in Lean (TPiL): Canonical reference for Lean. Great for introducing the basics of dependent type theory and how to work in it using Lean.
- Mathematics in Lean: Companion volume to TPiL, and has a greater emphasis on tactics and doing mathematics in Lean.
- The Hitchhiker’s Guide to Logical Verification: Slightly more advanced presentation, with a view towards CS applications.
- Koundinya Vajjha (@kodyvajjha)
- Ashvni Narayanan (@laughinggas)