| Time | Speaker | Title | Resources | |
|---|---|---|---|---|
| 09:30 to 09:45 | Prof. Rajesh Gopakumar and organisers (ICTS-TIFR, India) | Welcome remarks | ||
| 09:45 to 10:45 | Filippo Nuccio (Université Jean Monnet, France) | How To Enjoy A Mathematical Discussion With Your Laptop | ||
| 11:00 to 12:45 | All speakers | Guided labs in Lean | ||
| 14:00 to 16:00 | - | Guided labs in Lean | ||
| 16:15 to 17:15 | Bhavik Mehta (Imperial College, London, UK) | Real-time formalization |
| Time | Speaker | Title | Resources | |
|---|---|---|---|---|
| 09:30 to 11:00 | Ricardo Brasca (Université Paris Cité, France) | Finding theorems in Lean and Mathlib | ||
| 11:15 to 12:45 | - | Guided labs | ||
| 14:00 to 14:15 | Siddhartha Gadgil (IISc, India) | Programming in Lean | ||
| 14:15 to 16:00 | - | Guided labs in Lean | ||
| 16:15 to 17:15 | Anne Baanen (Lean FRO, LLC) | Redoing definitions in the Lean Mathematical Library |
| Time | Speaker | Title | Resources | |
|---|---|---|---|---|
| 09:30 to 10:30 | Patrick Massot (Université Paris-Saclay, France) | The Sphere Eversion Project | ||
| 10:45 to 11:45 | Filippo Nuccio (Université Jean Monnet, France) | Formalising Local Fields | ||
| 11:45 to 12:45 | Patrick Massot (Université Paris-Saclay, France) | Lean for Teaching | ||
| 12:45 to 13:00 | Ashvi Narayanan (University of Sydney, Australia) | Invitation to Math-AI and Lean-Math-AI | ||
| 14:00 to 15:00 | - | Guided labs |