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
LEAN for PDEs - ICARM & SLMATH
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.
LEAN for PDEs - ICARM & SLMATH
Please report video problems to itsupport@slmath.org.
See more of our Streaming videos on our main VMath Videos page.