MA 207: Proofs Lab with Lean
Credits: 0:1
The goal of this course is to help students learn to write rigorous mathematical proofs, with the Lean Prover used as a tool. We emphasise that writing proofs in Lean is not the goal, but merely a means to help students write better proofs for human readers. The course will be for 1 credit (0:1) and enrolment will be limited.
Specifically we use Verbose Lean, a controlled natural language for Lean developed by Patrick Massot and successfully used in Orsay for such a course. Working with the Lean Prover (with Verbose Lean) is helpful in learning to write proofs as:
- Lean will only accept a proof that is correct and sufficiently detailed.
- At each step the user is shown in a convenient way what is required, what has been proved, what are the assumptions etc.
- As the proofs in Verbose Lean look like natural language, so students can rewrite as informal proofs.
The course will consist of a weekly lab session where students work out exercises where they write formal proofs in Lean and then rewrite these as informal proofs to be read by a person. This is meant for students who have seen proofs but are not yet adept at writing them, for instance undergraduates in their fourth semester.
Sources
- The Lean language: https://lean-lang.org/
- Verbose Lean: https://github.com/PatrickMassot/verbose-lean4
- Exercises: https://github.com/PatrickMassot/proofs_with_lean