Interactive Theorem Proving in Lean (Spring 2022)
Motivation
Computers have played an essential role in the proof of various important theorems like the four color theorem (1976) and the Kepler conjecture (1998). However, their use was restricted to arguments that only required a lengthy mechanical case analysis.
Nowadays, interactive theorem provers allow the verification of virtually any mathematical theorem in a collaborative effort between machine and human; the most prominent such proof assistants are Coq, Isabelle, and Lean. In practice, few theorems at the level of present research have been formally checked by these tools, but the practical possibility has been demonstrated in some cases, for example with the formal verification of the Kepler conjecture in 2017 and the very recent success within the liquid tensor experiment proposed by Scholze.
Unfortunately, the translation of a proof in a mathematical textbook or article to one that is verifiable by a proof assistant can still be a very tedious task, requiring both skill and experience on behalf of the translator. In their argumentation, mathematicians often rely on intuition and a knowledge of many fundamental results. In recent years, the Lean community has built a mathematical library containing basic proof tactics and verified proofs, which should eventually cover at least the complete curriculum of an undergraduate student in mathematics.
Project Description
In this project, we study the Lean Theorem Prover whose first version (written by Leonardo de Moura, Microsoft Research) came out in 2013 and that is now available in its fourth version. (For practical reasons, we will use Lean 3 instead of the most recent version Lean 3.) In recent years, a substantial mathematical library (i.e., a collection of formalized definitions and proofs in Lean) has been built by the Lean community. Our aim will be to get a first working knowledge of both.
The project falls in three phases (preliminary plan, there may be changes!):
(1) exploring the Lean programming language (approx. 3 weeks):
a pragmatic introduction to the basic features of Lean (formal proof verification, dependent type theory, calculus of constructions)
(2) exploring undergraduate mathematics in Lean (approx. 3 weeks):
a look at some actual ``undergraduate'' mathematics done in Lean; tutorials with ``real mathematics''; identification of topics for own projects
(3) own projects (approx. 6 weeks):
work on specific problems; in-person-meeting in Copenhagen
Time Frame
12 weeks in total, submission deadlines after agreement between the participants and the coordinator
Prerequisites
The students
have a mastery of first year undergraduate mathematics,
appreciate rigorous formal mathematical arguments and proofs, such as those that one should encounter in first year lectures, e.g. epsilon-delta-arguments,
are able to set up a working environment for Lean 3 on their computer, following instructions,
(optimally) have already some basic exposure to Lean (e.g., by trying to play the natural number game),
(optimally) have programming experience, even better if in a functional programming language (e.g., Haskell).
Note that the learning curve during the project may be steep so that enduring motivation for the topic is required.
Learning Outcomes
After a successful participation, the students will be able to
use dependent type theory (instead of set theory) as a foundation of mathematics,
read and write correct, maintainable Lean code,
translate mathematical theorems (in the context of an undergraduate curriculum) to Lean definitions and theorem statements,
use basic strategies to verify such theorems in Lean by translating and adapting proofs from textbooks,
search and find results in the mathematical library of Lean (mathlib),
communicate problems, goals, and ideas to other members of the Lean community.
Workload
In the first (and most of the second) phase, we will meet regularly twice a week, for a total of approx. 180 minutes per week. In later phases, we meet as needed. It is expected that you do tutorial exercises (some in the form of two assignments) as well as acquire some information from Theorem Proving in Lean on your own -- in addition to our meetings. For the third stage of the project, you should be prepared to code about 5-8 hours a week.
Evaluation
(preliminary information, to be confirmed:) Students receive a Danish grade (12, 10, 7, 4, 02, 00, -3). For information on the Danish grading scale, please refer to this website. You will receive a grade a for the assignments (tutorial exercises) and a grade b for the work on your own project (code + written report + oral presentation). The final grade is then a/3+2b/3, rounded to the next grade (up in case of equidistance).
If you receive a numerical grade for this project with your local university, some conversion schemes will be applied. If you only receive a pass/fail, then all grades except 00 and -3 mean a pass.