This site collects announcements and files related to the course Formalizing and Proving Theorems in Coq, as taught by me in the Master of Logic at the ILLC in June 2022.
A formal proof of a theorem starts from a given set of premises, and then applies logically sound rules to reach the desired conclusion. It is typically understood that such a proof could, in principle, be mechanically checked by a machine, to see if no extra assumptions were made, and each of the rules was applied correctly. Proofs encountered in the literature, on the other hand, are usually rendered in natural language. This opens up the risk of human error — perhaps an induction hypothesis was applied incorrectly, the author forgot to cover a certain case, or some additional assumption was made inadvertently.
Proof assistants help bridge this gap, by providing the user with a rigorous, machine-checked language to encode their assumptions, claims, and proofs. In fact, modern proof assistants are general and flexible enough to express complicated arguments, such as proofs of the Kepler Conjecture and the Four Color Theorem. Furthermore, proof assistants facilitate the interactive exploration of possible arguments, and may also help to automate the "boring parts" of an argument, allowing the user to focus on steps that require creativity.
In this course, you will learn how to use the Coq proof assistant. The first half will be spent on lectures and exercises aimed at gaining a basic familiarity with Coq itself. We will see how common mathematical formalisms can be encoded, and how you can write and discover proofs interactively. In the last two lectures, we will encounter some more advanced topics such as dependent types, and the correspondence between programs and proofs (known as the Curry-Howard isomorphism), although we will not treat these subjects in detail.
In the second half of the course, you will choose a theorem whose proof you already know, and formalize it in Coq. Over the course of this project, the instructor will be available to answer your technical questions. The course will be concluded by a series of short talks on the projects by you and your peers, showcasing your formalization and the difficulties you encountered.
NB: This course complements Logical Verification (which uses the Lean proof assistant), and focuses more on enabling you to use a proof assistant in your area of interest, but less on programming language theory. Students interested in this general area are recommended to consider taking both courses.
The course will be assessed as fail/pass based on homework exercises, final presentations (roughly 30 minutes), and lecture attendance.
Students should be comfortable with common proof strategies such as induction, case distinction, and proof by contradiction. Some familiarity with (functional) programming will be useful, but is not strictly required.
Some students consented to sharing their final code and slides online: