Automatic theorem proving using Lean (COL876/COL8271 – Special Topics in Formal Methods)

Automatically generating and verifying proofs of correctness has been steadily gaining prominence in mathematics and computer science, especially with LLMs pervading all aspects of our lives. Proof assistants like Rocq and Lean are at the forefront of this effort, but being able to generate proofs of correctness requires a lot of scaffolding and the encoding of fundamental structures to build things up from the ground up. This course is designed to be a primer to learn how to write proofs in the proof assistant Lean.

In this course, we will see how to encode basic discrete structures like graphs, trees, and orders in Lean, and prove theorems about them. This will give us a hands-on introduction to Lean and the way various constructs work in Lean, and we will slowly build up to proving statements about more complex data structures and algorithms, with a view to how such proofs can be used in mathematics and computer science. We will also get a flavour of how Lean works behind the scenes, and the dependent type theory that is used for it. Finally, we will look at GenAI techniques for Lean, and see if we can use some of these to generate (correct) proofs of interest.

You should have some working understanding of the syntax of propositional/first order logic, a basic idea of what graphs and orders are, and an interest in coming up with rigorous mathematical proofs. It is helpful to have done a discrete mathematics course, but not necessary.

• In-class quizzes: 0–5%
• Programming test(s): ˜20%
• Minor exam: 20%
• Final project + deliverables: ˜55%

Audit policy: Audit pass needs at least a B- overall, including at least 30% in the final project.