There will be many events related to Formalisation, Lean Theorem Prover and AI for Mathematics at IISc between Monday, April 21, 2025 and Wednesday, April 23, 2025. These are organised/supported by Kotak IISc AI-ML Centre.
There will be three kinds of events. Except for the symposium in the Faculty Hall, all events will be at LH-3, Department of Mathematics, IISc.
- Talks: A symposium with three talks plus three separate talks
- Lean project discussion: Students who are working on Lean projects will present for discussion on improvements, fixes, future work etc. Those taking the course Proofs and Programs will present. Others are welcome to present.
- Lean Labs: Informal, weakly structured meetings to learn and/or work together on various aspects of Lean, Mathlib and Lean tooling (more details below).
Monday, April 21
- 10:00–12:00 : Lean Projects discussion
- 2:00–5:15 : Symposium on Formalisation, Mathematics, and Artificial Intelligence at the Faculty Hall, IISc:
- 2:00–3:00 PM: Koundinya Vajjha, Formal Verification for Mathematics, Software, and Hardware
- 3:00–4:00 PM: Bhavik Mehta, Mathematics, AI, and Lean
- 4:00–4:15 PM: Coffee break
- 4:15–5:15 PM: Patrick Massot, Why Formalise Mathematics?
Tuesday, April 22
- 9:00–11:00 : Lean Labs
- 11:00–12:00 : Anne Baanen, Certifying Algebraic Number Theory Computation
- 2:30–3:30 : Filippo Nuccio and Ricardo Brasca, Formalising Class Groups and Fermat’s Last Theorem for Regular Primes
- 4:00–5:00 : Patrick Massot, Lean for Teaching
Wednesday, April 23
- 9:00–12:30 : Lean Labs
- 2:00–4:00 : Lean Projects Discussion
- 4:00–5:00 : Ashvi Narayanan, Opportunities in Math-AI and Lean-Math-AI
Lean Labs:
These will be informal sessions consisting of:
- Demos/Tutorials/Deep dives
- Getting together to work on something specific
Where the topics can be:
- Specific techniques, tools etc in Lean (or AI for Mathematics)
- Specific topics for Lean/Mathlib
The plan is to mix presentations to everyone and break-outs into smaller groups. All are welcome to suggest topics that they want to learn or work on. Some of the topics suggested/planned so far are:
- Proofs of primality for large numbers
- Knot theory
- Number theory in Mathlib
- Widgets
- Autoformalization
- Meta-programming