Summary ​

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 four 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).

Workshop repo ​

All the Lean code for the workshop, the exercises and the slides from each talk are available in the event repo.

Schedule ​

The colloquium talks will be held in room 2001 and the workshop sessions in Aula 26.

Colloquium talks ​

• How to enjoy a mathematical discussion with your laptop
  • by Filippo A. E. Nuccio Mortarino Majno di Capriglio
  • Abstract: In this talk I will illustrate how certain programs, of which Lean is an example, permit to interact with a computer about the logical soundness of mathematical arguments. I will go through the details of well-known proofs trying to understand the feedback provided by the computer and will try to share the fun involved in the process.
  • Wed 24/01/2024, 15:30-16:30, room 2001 (talk slides)
• The internals of Lean
  • by Floris van Doorn
  • Abstract: In this talk I will describe what goes on behind the scenes of Lean. I will explain the logic of Lean, called dependent type theory, what Lean tactics are and explain why we can trust proofs that are checked by Lean.
  • Thu 25/01/2024, 12:00-13:00, room 2001 (talk slides)
• The benefits and challenges of teaching proof with Lean
  • by Gihan Marasingha
  • Abstract: This presentation will explore the pivotal role of Lean in enhancing first-year undergraduates' understanding of mathematical proofs. I will share insights from my experiences and initial educational research on teaching a large first-year undergraduate cohort with Lean, focusing on how this tool can significantly impact student perception of proofs. Additionally, I will address the challenges encountered in teaching with Lean and the implications for learning and comprehension.
  • Thu 25/01/2024, 14:30-15:30, room 2001 (talk slides)
• Formalising modern research mathematics (Departmental Colloquium)
  • by Kevin Buzzard
  • Abstract: A few years ago, the idea of formalising modern research level mathematics seemed completely out of reach. Since then, more and more examples have appeared. I'll go through several examples (some related to the mathematics of Scholze, Tao and Gowers), and talk about how the process is evolving, enabling multiple people to collaborate in the formalisation of modern research in real time.
  • Fri 26/01/2024, 14:30-15:30, room 2001 (talk slides)

Speakers ​

• Riccardo Brasca
• Kevin Buzzard
• Floris van Doorn
• Gihan Marasingha
• Filippo A. E. Nuccio Mortarino Majno di Capriglio

See also the event team page.

Participants ​

Alessio Proietti, Amos Turchet, Carlangelo Liverani, Christoph Lhotka, Daniel K Lou, David Wiygul, Fabrizio Barroero, Fedor Part, Gabriele Gullà, Giovanni Canestrari, Giulia Cava, Guido Lido, Laura Capuano, Lorenzo Luccioli, Luca Ferrigno, Luca Giorgetti, Marco Lenci, Marco Pedicini, Marco Pozza, Minsung Kim, Nicola Ottolini, Oliver Butterley, Pietro Monticone, Rafael Greenblatt, Rinat Kamalov, Roberto Castorrini, Valerio Dose, Valery Isaev, Vincenzo Bonifaci, Vincenzo Morinelli, Yoh Tanimoto.

Practical info ​

The Mathematics department of the University of Rome Tor Vergata is not the easiest place to reach from the city centre. Our advice on public transport is to get to the Anagnina stop of Metro Line A and take the 20 or 500 (Atac) bus from there. They stop at several locations within or near campus (@). It's easiest (by far) that you get off at the right stop, the one near the "Macroarea di Scienze Matematiche Fisiche e Naturali (M.F.N.)", which is the building that hosts the Mathematics Department (together with other departments).

Here’s a Google map pointer to the building, that you can use to plan your trip, identify the right stop once you’re on the bus, etc. See also here for more transportation info.

Register ​

In case you are interested, please register. (Update 06/01/2024: we will do our best to accommodate everyone who wishes to attend, if registering very close to the event, please contact us if you don't hear back within a few days of registering.)

Contact ​

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

Links ​

• 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.
• To use the Lean files in the cloud, open the project in Codespaces. Note that this requires a Github account. Make sure the Machine type is 4-core, and then press Create codespace. After 1-2 minutes you see a VSCode window in your browser. However, it is still busily downloading mathlib in the background, so give it another few minutes (5 to be safe) and then open a .lean file to start.

Supporters ​

• MUR Excellence Department Project MatMod@TOV awarded to the Department of Mathematics, University of Rome Tor Vergata, CUP E83C23000330006.
• PRIN Grant "Regular and stochastic behaviour in dynamical systems" (PRIN 2017S35EHN).