Computational proof assistants now make it possible to develop global, digital mathematical libraries with theorems that are fully checked by computer. This summer school will introduce students to the new technology and to the goals and benefits of formalized mathematics, including metaprogramming and autoformalization. Students will learn to use the Lean interactive proof assistant, and by the end of the session, they will be in a position to formalize mathematics on their own, join the Lean community, and contribute to its mathematical library.

School Structure

On the first day, students will be provided with an overview of the technology and help with installing Lean on their laptops. After that, the general format of the school will be to interweave short lectures with long, interactive tutorial sessions. Some general lectures on the theory and practice of formalization will give students a glimpse of activity in the field. During the second week, students will also work on independent formalization projects in small groups. They will have the opportunity to share their results, report on their progress, and receive feedback from their peers. Optionally, students will be able to participate in a series of tutorials on metaprogramming to learn how to write Lean tactics and automation.

Suggested prerequisites

• At least one undergraduate level computer programming course
• A mathematical area of interest that will be the focus of the student’s formalization project