Metaprogramming in Lean tutorial

Johan Commelin and Patrick Massot are organizing the workshop Lean for the Curious Mathematician, taking place virtually July 13-17, 2020. The workshop aims to give working mathematicians a hands-on introduction to formal proof.

As part of the “intermediate track” of this workshop, for users who have some experience with formal proof, I recorded a series of videos about metaprogramming in Lean: how do we use the system to introspect on its own syntax and write and evaluate programs to prove theorems?

Since the workshop is aimed at a novice audience, I wasn’t expecting a large live audience, so I prerecorded the videos and put them on YouTube. The first two videos in the series are accessible to people who have had any introduction to Lean, for instance through the Natural Number Game. The later videos assume some more familiarity with the system and with functional programming.

Feedback on these recordings is very welcome!