∀∃  Lean Together 2024  ∃∀ A meeting all about Lean

Talks will run for around four hours each day (including breaks). We will stagger the start times to accommodate different time zones.

Social time on Gather will run during the coffee breaks and after each day’s talks.

We have scheduled a mix of casual and more formal presentations, comprising a live program and a collection of prerecorded talks. Talks were selected to create a balanced, interesting, and diverse program rather than by ranking each proposal in a fixed order.

Live program

Recordings of all talks are on the Lean community YouTube channel.

Times below are displayed in your browser time zone, . The first talk of the workshop is scheduled for 14:00 GMT. You can also view the schedule on https://researchseminars.org.

Prerecorded talks

In addition to the live program, we have hosted a number of prerecorded talks. Look for the speakers during the designated social hour to chat about their presentations!

Speaker Talk Social hour Q&A
Alex Oltean Towards a Completeness Proof of Hybrid Modal Logic Wednesday, Jan 10
Shashank Pathak Autoformalization via Grammatical Framework Wednesday, Jan 10
Jack McKoen Simplicial Homotopies in Lean Thursday, Jan 11
Bolton Bailey Formalization of SNARKs Thursday, Jan 11