Lean in Lyon

Lean in Lyon

Institut Camille Jordan
Villeurbanne, campus de la Doua
salle  Fokko du Cloux

Une journée dédiée à la formalisation mathématique.


Lean in Lyon



Le but de cette journée est de réunir des mathématiciens travaillant sur Lean, l'assistant de preuve de la bibliothèque mathlib. Les exposés s'adresseront à un public large : tous les chercheurs curieux des développements récents en formalisation sont bienvenus.

The aim of this workshop is to gather together several mathematicians working on Lean, the proof assistant of the mathematical library mathlib. The talks will focus on engaging all mathematicians who are curious to discover the recent developments of formalization.



Filippo Nuccio, Institut Camille Jordan, Université Jean Monnet



Riccardo Brasca, Institut de Mathématiques de Jussieu-Paris Rive Gauche, Université de Paris,
Johan Commelin, Mathematisches Institut, Albert-Ludwigs-Universität Freiburg,
Floris van Doorn, Laboratoire des Mathématiques d'Orsay, Université de Paris-Saclay,
Sébastien Gouëzel, Institut de Recherche Mathématique de Rennes, Université de Rennes,
Patrick Massot, Laboratoire des Mathématiques d'Orsay, Université de Paris-Saclay.




10h00-11h00 : Patrick Massot

Title: Formalized mathematics and differential topology

Abstract:  In the first part of the talk, I will show how to explain a proof to a computer using a software called Lean. This process called formalization is well known to be applicable to algebra or combinatorics. For example the team of Georges Gonthier and Assia Mahboubi explained to the software Coq the Feit-Thompson theorem, a very famous result about finite groups. In the last few years, the field of application of these methods has considerably widened. Together with Floris van Doorn and Oliver Nash, I am currently formalizing enough differential topology to cover in particular the existence of the famous sphere eversions. In the second part of my talk I will present this project and its mathematical context. Floris van Doorn's talk will then explain some of the surprises encountered along the way.

11h15-12h15 : Riccardo Brasca

Title : Fermat's Last Theorem for regular primes in Lean


Abstract: I will speak about an ongoing project whose goal is to formalize, in Lean, Kummer's proof of Fermat's Last Theorem for regular prime exponents. This was a landmark 19th century result in algebraic number theory, proving the theorem in many new cases at the time. I will explain why this is useful, both for standard and formalized mathematics. In particular, I will focus on the difficulties we faced during the formalization process, and how we solved them. No prior knowledge of formalized mathematics or of the pen and paper proof is needed to understand the talk.

14h00-15h00  : Sébastien Gouëzel  

Title: Changing variables in integrals and in Lean

Abstract: the change of variables formula in integrals is a basic tool in analysis, often presented in a standard undergraduate curriculum. I have formalized recently a version of this theorem in mathlib. This formalization raised several interesting questions, notably on the suitable level of generality of this theorem. In this talk, I will present a math journey through several possible versions of this theorem, with tools ranging from Gaussian elimination on matrices to Haar measure and descriptive set theory of Polish spaces. The accent will be put more on the mathematical side of the story than on the formalization side, although some issues that are specific to formalization will be discussed.

15h15-16h15 : Johan Commelin  

Title: Reflection on the Liquid Tensor Experiment

Abstract: In this talk I will present a medley of reflections on the Liquid Tensor Experiment. What worked well? What can we learn for future projects? The talk will be an informal mix of maths and computer science.

16h30-17h30 : Floris van Doorn 

Title:  Lessons learned from formalizing local convex integration 


Abstract:  I will present the current progress that Patrick Massot, Oliver Nash and I have made towards formalizing convex integration in Lean, with as immediate corollary the existence of sphere eversions. I will discuss the challenges of formalizing differential topology and discuss the techniques we have used to make the formalization nicer, including a general definition of the convolution of functions. No background knowledge of formalization or differential topology is assumed.



Lundi 9 mai 2022,  Johan Commelin, Mathematisches Institut, Albert-Ludwigs-Universität Freiburg, parlera au colloquium de l'ICJ

May 9, 2022, Johan Commelin, Mathematisches Institut, Albert-Ludwigs-Universität Freiburg, will give a talk at the ICJ Colloquium





Le workshop se déroulera à l’Institut Camille Jordan  / Université Claude Bernard Lyon 1,sur le campus de la Doua
bâtiment Braconnier
43, Bd du 11 novembre 1918 à Villeurbanne,
dans la salle Fokko du Cloux (premier étage).
Accès au site de la Doua

The workshop will take place at the Institut Camille Jordan / Claude Bernard Lyon 1 University, La Doua Campus
entrance Braconnier
43, Bd du 11 novembre 1918, Villeurbanne,
in room Fokko du Cloux (1st floor).
How to come

Pour plus d'informations, for further information : Filippo Nuccio (filippo.nuccio @ univ-st-etienne.fr)