You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Fernando Chu (Mar 10 2025 at 13:17):Summer School on Formalizing Mathematics in Lean
Director: Johan Commelin
Organisers: Christian Merten, Fernando Chu, Raphael Douglas Giles
We are pleased to announce a summer school on formalizing mathematics in Lean, which will take place at Utrecht University, Utrecht, the Netherlands, from 21 July to 25 July 2025.
Interactive theorem provers assist in the development of mathematical proofs by verifying and automating proof steps. Formalizing mathematics involves expressing mathematical arguments in a precise language that such systems can understand. In recent years, an increasing amount of mathematics, from undergraduate topics to cutting-edge research, has been formalized in various proof assistants.
This course will focus on Lean and its mathematical library, mathlib. Participants will learn how to formalize mathematical proofs and gain hands-on experience with Lean’s proof automation tools. This will enhance students' mathematical abilities and allow them to contribute to mathlib.
The course is aimed at students familiar with rigorous mathematical reasoning who have an interest in theorem proving. It is particularly suitable for those in the later stages of a bachelor’s degree or pursuing a master's or PhD in mathematics, computer science, physics, or related fields.
The participation fee for students is €200, which covers lunch and coffee breaks. If accommodation is required, this is also available for an additional fee.
For more details and registration, please visit:
https://utrechtsummerschool.nl/courses/science/formalizing-mathematics-in-lean