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.
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.
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 |