Interactive Session
Lean for PDEs, an ICARM & SLMath collaboration October 06, 2025 - October 09, 2025
Location: SLMath: Eisenbud Auditorium
Primary Mathematics Subject Classification
No Primary AMS MSC
Secondary Mathematics Subject Classification
No Secondary AMS MSC
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.