Bridging Formal & Informal Proofs
The goal of this course is to help students learn to write rigorous mathematical proofs, utilizing the Lean Prover as a foundational 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.
Why Verbose Lean?
Specifically, we use Verbose Lean, a controlled natural language for Lean developed by Patrick Massot. This approach has been successfully used in Orsay for similar courses. Working with the Lean Prover (with Verbose Lean) is helpful in learning to write proofs because:
Guaranteed Correctness
Lean will only accept a proof that is logically correct and sufficiently detailed, eliminating ambiguity.
Immediate Feedback
At each step, the user is shown exactly what is required, what has been proved so far, and what assumptions are active.
Natural Language Bridge
Proofs in Verbose Lean look like natural language, allowing students to seamlessly rewrite their formal work as informal proofs for human readers.
Course Format & Audience
The course consists of a weekly lab session. Students will work out exercises by:
- Writing formal proofs in Lean.
- Rewriting these as informal proofs to be read by a person.
Who is this for?
This course is meant for students who have seen proofs but are not yet adept at writing them (e.g., undergraduates in their fourth semester). Enrollment is limited.
Installation Instructions
1 Installing VS Code and Lean 4
Follow the official instructions at the Lean 4 Quickstart Guide to install Visual Studio Code and the Lean 4 plugin. Verify that the installation is working.
lean4), not the “Lean 3” one (called lean).
2 Downloading the Course Repository
As you have seen in the previous step, the menu for the Lean 4 plugin is at the ∀ symbol.
- At the Lean 4 (∀) menu, choose “Open Project”, then “Download Project”.
- Choose the repository: https://github.com/siddhartha-gadgil/proofs_with_verbose_lean
- Open the file
Exercises/f01_equalities_inequalities.leanto check that the installation has worked.
Important Links
The Lean Prover
Official website of the Lean functional programming language and theorem prover.
Online Playground
Run Verbose Lean directly in your browser without installation (IISc LAN/WIFI or VPN).
Course Repository
Contains exercise sheets, code samples, and lab templates.
Zulip Community
Join the Automath India community discussion.
Microsoft Teams
Official course channel (Link coming soon).