An interactive theorem prover is a computer program to assist with the development of mathematical proofs. By checking and automating proof steps, the machine aides the user in creating proofs in a formal language understandable to the program.
Formalizing mathematics is the process of typing mathematical proofs into the interface of an interactive theorem prover. In the past years, more and more mathematics, from undergraduate level to the frontiers of modern research have been formalized in a variety of proof assistants.
While there are many interactive theorem provers, this course focuses on Lean and its mathematical library mathlib, which already contains a substantial number of proofs of mathematical theorems and infrastructure for proof automation.
The course is targeted to students familiar with rigorous mathematical proofs (e.g. careful proofs by induction) that have an interest in theorem proving in Lean.
Students in science (mathematics, computer science, physics, etc) that are coursing the second half of their bachelor, or are doing a MSc or a PhD will be well prepared for this course.
The registration fee is 200€ for students and covers lunch and coffee breaks. Housing can be organised via the Utrecht Summerschool Team.
For more information and registration please head to the registration page.
See Schedule.