Talks

Error message

Lean for the Curious Mathematician
Thursday, 24 April 2025
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
 
Friday, 25 April 2025
Time Speaker Title Resources
09:30 to 11:00 Ricardo Brasca (Université Paris Cité, France) Finding theorems in Lean and Mathlib

Mathlib is a vast and constantly growing library of formalized mathematics. As its size increases, it becomes increasingly easy to spend a significant amount of time formalizing a theorem, only to later discover that it was already present in the library. This can be both frustrating and discouraging. In this talk, we will introduce and demonstrate a variety of tools and techniques that can help users efficiently navigate Mathlib, search for existing results, and better understand the structure of the library.
 
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

Mathematicians have trained themselves to see objects from many points of view. When considering the real numbers, we can as easily see them as equivalence classes of Cauchy sequences, or Dedekind cuts, or the unique uniformly complete Archimedean field. The computer is not as forgiving and forces us to pick a particular definition that we must stick with. Using examples from the Lean mathematical library, Mathlib, I investigate why it is so important to choose the right definition when formalizing, what makes formal definitions look different from pen and paper definitions, and how we can design our definitions to make proofs flow smoothly.
 
Saturday, 26 April 2025
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

I will describe how the Lean proof assistant software can be used to teach mathematical reasoning to young students at university. This is different from teaching how to use Lean. Here Lean is only a tool, not the end goal.

I will explain what we can hope to teach using this tool, what are the available resources for teachers, and what choices should be made. I will then show my teaching library, Verbose Lean, which uses controlled natural language and customizable automation to optimize transfer of skills to paper proofs.
   
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