Some basic concepts in mathlib and the dependencies between them

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 the ideas behind it, and will encourage them to think about the goals and benefits of formalized mathematics. 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.

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

For eligibility and how to apply, see the Summer Graduate Schools homepage