Formal methods in Mathematical proof

Monday 23rd June, Newman Collaborative (WSFM1)

15:10 – 16:10 Bhavik Mehta (Imperial)
16:10 – 17:10 Athina Thoma (Southampton)

Tuesday 24th June, Newman Collaborative (WSFM2)

15:40 – 16:40 Chris Birkbeck (East Anglia)
16:40 – 17:40 Yaël Dillies (Stockholm)

Wednesday 25th June, Newman Red (WSNT3)

Chris Birkbeck – Formalising modular forms and sphere packings in Lean
I will discuss some work on formalising modular forms in Lean and how it is used in our (ongoing) formalization of Maryna Viazovska’s Fields Medal-winning paper proving that no packing of unit balls in Euclidean space $\mathbb{R}^8$ has density greater than that of the $\mathrm{E}_8$ -lattice packing. Part of this is joint work with Sidharth Hariharan, Gareth Ma, Bhavik Mehta, Seewoo Lee and Maryna Viazovska.

Yaël Dillies – Why should Mathlib know about toric varieties?
Varieties, the basic objects of study in algebraic geometry, form a vast and complex world which is a priori difficult to grasp. Toric varieties are a special class of varieties which can be understood through combinatorial (and therefore computational) means, they are a rich source of examples of varieties and an indispensable tool for modern research in algebraic geometry and moduli spaces. Mathlib, the large library of formal mathematics built using the Lean theorem prover, now contains most of a standard undergraduate curriculum, and in particular varieties (or more generally, schemes). In this talk, I will report on the current effort to teach Mathlib about toric varieties and the lessons we learned along the way. I will also outline how to contribute to the project. Basic knowledge of algebraic geometry will increase enjoyment, but won’t be assumed. Joint work with Michał Mrugała (ENS Lyon), Andrew Yang (ICL) and the other Toric contributors.

Athina Thoma – Using Lean in university mathematics teaching: Insights and challenges
Interactive Theorem Provers (ITPs) like Lean are being integrated into university mathematics teaching, either as compulsory or optional addition. This talk presents educational research on how first-year undergraduates engage with Lean, drawing on analysis from their pen-and-paper proofs, activity with Lean, and their reflections. I will discuss the challenges students encounter, the learning opportunities Lean affords, and insights from lecturers who integrated Lean into an introductory proof course.