Lean Together 2021 A meeting for Lean users and other formalizers

A meeting for Lean users and other formalizers

Virtually via Zoom: 4—7 Jan 2021


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 speakers and participants from other proof assistant communities, as well as people who are inexperienced with proof assistants but want to learn more.

This year, due to world events, the meeting will be virtual. The event is open to everyone without cost: feel free to attend as many sessions as you’d like.


The meeting will be held via Zoom, in a number of sessions spread out over the week of January 4. We will vary the starting times of the sessions to accommodate people in different time zones.

We will have a mix of shorter talks about work in progress, longer talks about more mature projects, and some open discussion/planning sessions. We will also have social time on gather.town before and after the sessions.

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: