Skip to content
On this page


In recent years computerized tools for verifying and manipulating proofs have become much more mature, and as a result formalized proofs are playing a meaningful role in mathematical innovation and teaching.

This short program consists of three colloquium talks on major aspects of formalization, in terms of both underlying ideas and concrete implementations, together with a series of workshop-style sessions intended to give participants first-hand knowledge using the Lean language, its mathematical library and associated tools. We aim to provide an introduction to the area for working mathematicians and advanced students in a variety of fields.

Copious quantities of coffee ☕ and space to code and collaborate will be available.

Workshop and talks will be held in the Department of Mathematics, University of Rome Tor Vergata (Via della Ricerca Scientifica 1, 00133 Roma).

Schedule & speakers

Wed 24/01/2024Thu 25/01/2024Fri 26/01/2024
11:00-12:00☕ 💻☕ 💻
12:00-13:00workshopColloquium 2workshop
14:30-15:30workshopColloquium 3Colloquium 4
15:30-16:30Colloquium 1☕ 💻☕ 💻
16:30-17:30☕ 🍷workshopworkshop
Session topics (tap to view)
1introductionRiccardotutorial on Lean, installation of Lean (if needed), topics in mathlib (ch 1)
2basicsGihanapply, rewrite, linarith (ch 2)
3&4logicRiccardological connectives and quantifiers (ch 3)
5sets, functionsFilippointersections, (pre)images, extensionality (ch 4)
6&7topologyFloristopological spaces, filters (ch 9)

Chapter numbers listed are from Mathematics in Lean.


See also the event team page.

Colloquium talks

Colloquium 1Filippo A. E. Nuccio Mortarino Majno di CapriglioTBA
Colloquium 2Floris van DoornTBA
Colloquium 3Gihan MarasinghaTBA
Colloquium 4Kevin BuzzardTBA


In case you are interested, please register, sooner rather that later, it helps us a lot with the organization! (And it's fine if you change your mind.)


Contact Oliver Butterley or another of the local organizers for anything practical.

  • Getting started with Lean: If you haven't already, get started by installing Lean or using it online.
  • Other events of interests: For those who want to go deeper into Lean and mathlib, check out some other Lean events.

Department of Mathematics, University of Rome Tor Vergata.