School on Formal Mathematics

Dates: May 13 - 17, 2024
Venue: HIM lecture hall (Poppelsdorfer Allee 45, Bonn)
Organizers: Michael Kohlhase (Erlangen), Jacques Carette (Hamilton), Valeria de Paiva (Berkeley), Josef Urban (Praha)

Lecturers:

• TBA

Description:

This one-week school teaches practical theorem proving in the three proof assistants with the greatest coverage of (research) Mathematics: Coq, Isabelle and Lean as well as smaller, more specialized systems. Key people from the research groups have indicated their willingness to teach (and supervise practical formalization attempts) in this school, drawing on tutorial material of the various systems. Participants of the school will be asked to work on small formalization projects which eventually could lead to contributions to formalization libraries. There will be a couple of introductory and special lectures.

The online application platform to participate in this school is open until January 31, 2024.

Trimester Program guests, who were invited and have confirmed to be at HIM during the period of this workshop, are eligible to attend this event.