The workshop will take place virtually via Zoom, the week of Jan 4. We tried to schedule things acceptably for various timezones, starting at different times on different days.
We will start:
Sessions will last 4-5 hours including breaks.
Social time will be held on gather.town. We will open the room before and after each day’s events. The social time on Monday is “official”: if you’re only planning to attend one social event, try to make it this one.
We have created a YouTube playlist of all the talks. This will be updated as the workshop continues.
Some talks were added to our program too late to fit in the live schedule. We have included these as pre-recorded talks. Video links will be posted here. The speakers will be available during specified social hours to discuss their presentations: look for them on gather.town!
| Q&A Time | Speaker |
| Tuesday, Jan 5 |
Mario Carneiro MM1: A Lean-style proof assistant for Metamath Zero (tutorial) |
| Wednesday, Jan 6 |
Vaibhav Karve Axiomatic Geometry in Lean Model Theory in Lean |
| Thursday, Jan 7 |
Alex Best Automatically generalising theorems using typeclasses in Lean (slides) |
| Time | Speaker |
|---|---|
| Rob Lewis and Patrick Massot Opening remarks (slides) |
|
| Floris van Doorn Measure theory (slides) |
|
| Heather Macbeth An example of a manifold (slides) |
|
| Ed Ayers Widgets: interactive output in VSCode (slides) |
|
| Coffee break | |
| Leonardo de Moura and Sebastian Ullrich An overview of Lean 4 (Leo slides, Sebastian slides) |
|
| Lean 4 Q&A | |
| Discussion: porting mathlib to Lean 4 | |
| Social time (“workshop dinner”) |
| Time | Speaker |
|---|---|
| Jannis Limperg Towards general-purpose automation for Lean (slides) |
|
| Chris Hughes Word problem for one-relator groups |
|
| Coffee break | |
| Stanislaus Polu OpenAI Metamath GPT-f (slides) |
|
| Jason Rute and Jesse Han LeanStep: a dataset and environment for (interactive) neural theorem proving in Lean 3 (slides) |
|
| Coffee break | |
| Koundinya Vajjha CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq (slides) |
|
| Yury Kudryashov Dynamics on the circle |
|
| Social time |
| Time | Speaker |
|---|---|
| Paula Neeley Results in modal and dynamic epistemic logic (slides, repo) |
|
| Kenny Lau Formalizing Perfectoid Fields (slides) |
|
| Yasmine Sharoda Generative Tools for Library Building (slides, repo) |
|
| Coffee break | |
| Leonardo de Moura and Sebastian Ullrich Metaprogramming in Lean 4 (Leo slides, Sebastian slides) |
|
| Joe Hendrix Towards verified decompilation using Lean 4 (slides) |
|
| Coffee break | |
| Adam Topaz Baby steps toward formalizing results in anabelian geometry (slides, repo) |
|
| Peter Nelson Formalising matroids |
|
| Social time |
| Time | Speaker |
|---|---|
| Marie Kerjean Complex analysis through a hierarchy of real-analysis structures (slides) |
|
| Damiano Testa Mathematical insights from using Lean (slides) |
|
| Amelia Livingston Definitions: are some more equal than others? |
|
| Coffee break | |
| Alena Gusakov Formalizing Hall’s Marriage Theorem (slides) |
|
| Panel/discussion: Teaching with proof assistants Panelists: Jeremy Avigad, Jasmin Blanchette, Heather Macbeth, Gihan Marasingha, Patrick Massot, Julien Narboux |
|
| Coffee break | |
| Logan Murphy Provably Deductive Assurance Cases (slides) |
|
| Thomas Browning and Patrick Lutz Galois theory (slides) |
|
| Leonardo de Moura and Sebastian Ullrich Metaprogramming in Lean 4 (continued) |
|
| Social time |