Course
Formalizing Mathematics in Lean
This course is a hands-on introduction to formalizing mathematics in Lean, a state-of-the-art interactive theorem prover.
€500
Student fee
€200.00
Specifications
Description
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.
Target audience
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.
Aim of the course
Participants will learn how to formalize mathematics in Lean. The acquired knowledge will not only enable participants to contribute to Lean's mathematical library mathlib - it will also strengthen their understanding of mathematics.
Study load
The course takes one week, with a few hours of lectures per day. We will offer supervised lab sessions to practice with the material taught in the lectures.
In the second part of the week, participants will work on self-chosen formalization projects in teams with assistance and supervision by experienced Lean users.
Costs
- Course fee: €500.00
- Student fee: €200.00
- Included: Course + course materials + lunch
- Housing fee: €200
- Housing provider: Utrecht Summer School
We will charge a registration fee of € 500 (or € 200 for students) to cover our expenses. In the course fee, lunch and coffee breaks are included.
If this is problematic for you for any reason at all, please email the organisers and we can try to offer you a reduced rate or a fee waiver.
Additional information
The housing costs do not include a Utrecht Summer School sleeping bag and/or pillow. These are separate products on the invoice. If you wish to bring your own bedding, please deselect or remove the sleeping bag from your order once you apply for this course.