Formalization Workshop

The goal of this seminar is to learn the basics of formalization in Lean together. The event is meant to be interactive and aimed at beginners. Everyone is welcome to join.

When and where

Fridays 12:00–13:00

Room M311 of the Math Department in Regensburg.

You can also join remotely via Zoom. Contact the organizers to obtain the access code.

NOTE: Due to a conflict with the Windberg retreat, the first event will be on Friday, 23rd of October (second week of semester).

Program

We haven't decided a detailed program yet, and the direction of the activity will also depend on the participants' preferences. We'll start with a hands-on introduction to the Lean proof assistant, by playing the learning games collected in the Lean Game Server: https://adam.math.hhu.de/. You can play the games directly from your pc, there's no need to install Lean for that. The idea is to alternate between solving game levels collectively or in small groups.

Organization

The workshop is organized by Luca Terenzi and Tashi Walde