Lean Together 2021 A meeting for Lean users and other formalizers

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.

Prerecorded Talks

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)

Monday, January 4

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”)

Tuesday, January 5

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

Wednesday, January 6

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

Thursday, January 7

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