Patrick Massot and I are organizing the third annual Lean users meeting: Lean Together 2021!

The event will take place virtually January 4-7. We will have a variety of talks about formalizations, tools and infrastructure, and teaching with proof assistants. All are welcome to attend; we hope to see you there!

(A post-workshop update: we have a YouTube playlist of the week's talks!)