Oct 06, 2025
Monday
|
|
02:00 PM - 03:00 PM
|
|
Interactive Session
Rémy Degenne (Inria; University of Lille), Michael Rothgang (Rheinische Friedrich-Wilhelms-Universität Bonn)
|
- Location
- SLMath: Eisenbud Auditorium
- Video
-
- Abstract
This first workshop session will start with a presentation of the Lean theorem prover and its mathematical library Mathlib, highlighting what formalization can bring to mathematics. We will describe in particular how formalization has been used to check recent mathematical results and how it enables large collaborations. The participants will then be guided through their first Lean proofs: they will discover the Lean language, learn how to write theorems and master the essential Lean tactics they can use to prove them.
- Supplements
-
--
|
|
03:00 PM - 03:30 PM
|
|
Tea Break
|
- Location
- SLMath: Atrium
- Video
-
--
- Abstract
- --
- Supplements
-
--
|
|
03:30 PM - 04:00 PM
|
|
Interactive Session
Rémy Degenne (Inria; University of Lille), Michael Rothgang (Rheinische Friedrich-Wilhelms-Universität Bonn)
|
- Location
- SLMath: Eisenbud Auditorium
- Video
-
--
- Abstract
This first workshop session will start with a presentation of the Lean theorem prover and its mathematical library Mathlib, highlighting what formalization can bring to mathematics. We will describe in particular how formalization has been used to check recent mathematical results and how it enables large collaborations. The participants will then be guided through their first Lean proofs: they will discover the Lean language, learn how to write theorems and master the essential Lean tactics they can use to prove them.
- Supplements
-
--
|
|
Oct 07, 2025
Tuesday
|
|
02:00 PM - 03:00 PM
|
|
Interactive Session
Rémy Degenne (Inria; University of Lille), Michael Rothgang (Rheinische Friedrich-Wilhelms-Universität Bonn)
|
- Location
- SLMath: Eisenbud Auditorium
- Video
-
--
- Abstract
The Lean tutorial will continue where the first day stopped and will cover more ways to write proofs in Lean. Once all the basic proofs tactics are introduced, the second part of the tutorial session will focus on proving results that are relevant to PDEs. The participants will get an overview of what is already in Mathlib and what results are still missing to develop PDE theory in Lean. They will then come up with short projects to enhance the PDE library, which will be worked on during the remainder of the workshop.
- Supplements
-
--
|
|
03:00 PM - 03:30 PM
|
|
Tea Break
|
- Location
- SLMath: Atrium
- Video
-
--
- Abstract
- --
- Supplements
-
--
|
|
03:30 PM - 04:30 PM
|
|
Interactive Session
Rémy Degenne (Inria; University of Lille), Michael Rothgang (Rheinische Friedrich-Wilhelms-Universität Bonn)
|
- Location
- SLMath: Eisenbud Auditorium
- Video
-
--
- Abstract
The Lean tutorial will continue where the first day stopped and will cover more ways to write proofs in Lean. Once all the basic proofs tactics are introduced, the second part of the tutorial session will focus on proving results that are relevant to PDEs. The participants will get an overview of what is already in Mathlib and what results are still missing to develop PDE theory in Lean. They will then come up with short projects to enhance the PDE library, which will be worked on during the remainder of the workshop.
- Supplements
-
--
|
|
Oct 09, 2025
Thursday
|
|
02:00 PM - 03:00 PM
|
|
Interactive Session
Rémy Degenne (Inria; University of Lille), Michael Rothgang (Rheinische Friedrich-Wilhelms-Universität Bonn)
|
- Location
- SLMath: Eisenbud Auditorium
- Video
-
--
- Abstract
This third day is dedicated to group projects: the participants will formalize mathematical statements of their choice about PDEs that are missing from Mathlib. The Lean experts will guide and help the groups to formulate their mathematical goals in Lean and come up with the best way to formalize their proofs.
- Supplements
-
--
|
|
03:00 PM - 03:30 PM
|
|
Tea Break
|
- Location
- SLMath: Atrium
- Video
-
--
- Abstract
- --
- Supplements
-
--
|
|
03:30 PM - 04:30 PM
|
|
Interactive Session
Rémy Degenne (Inria; University of Lille), Michael Rothgang (Rheinische Friedrich-Wilhelms-Universität Bonn)
|
- Location
- SLMath: Eisenbud Auditorium
- Video
-
--
- Abstract
This third day is dedicated to group projects: the participants will formalize mathematical statements of their choice about PDEs that are missing from Mathlib. The Lean experts will guide and help the groups to formulate their mathematical goals in Lean and come up with the best way to formalize their proofs.
- Supplements
-
--
|
|
