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

A meeting all about Lean

Virtually via Zoom: 9—12 Jan 2024


Lean Together is an annual meeting for users, developers, and fans of the Lean proof assistant and its library mathlib. At this meeting we discuss ongoing projects in formalized mathematics and software verification, as well as infrastructure and outreach for Lean and its community. We welcome participants from other proof assistant communities, as well as people who are inexperienced with proof assistants but want to learn more.

The meeting is virtual and open to everyone without cost. Feel free to attend as many sessions as you’d like.


Please fill out our registration form and we’ll keep you updated as planning progresses.


The meeting will be held via Zoom, in a number of sessions spread out January 9-12. We will vary the starting times of the sessions to accommodate people in different time zones. View the schedule here.

In addition to the talks in our live program, we will host prerecorded talks and schedule Q&A time with the speakers. We will also have social time before and after the sessions on Gather.

With the speakers’ permission, talks will be recorded and posted to the leanprover community YouTube channel.

Discussions related to the event will happen on the Lean Zulip chat channel.

Previous events


Main organization by: