Community
The independently-run Lean Community Zulip chat is the central hub for everything Lean. Whether you are a new or experienced Lean user, it’s a welcoming place to ask questions, share ideas, and collaborate with other Lean users.
Looking for more support?
Lean community website - A community maintained website that hosts a variety of helpful resources and is the main reference site for working with Mathlib, Lean's extensive community-built library of mathematics.
Lean community YouTube channel - Hosts many instructional videos, lectures and guides recorded from conferences and workshops organized by the Lean community.
Proof Assistants on Stack Exchange - Q&A for questions about proof assistants, including Lean. This is a great place to find community-approved guidance on how to use Lean.
The Mathlib Initiative
The Mathlib Initiative is a program of Renaissance Philanthropy which provides professional support for editorial work, infrastructure development, and ecosystem coordination for the Mathlib project.
Events
Subscribe to the events iCal to track all listed events and get event information.
Office Hours
The Office Hours Google Meet is a weekly one-hour video call hosted by the Lean FRO to answer technical questions about Lean. Questions may be sent to officehours@lean-fro.org in advance, or through the associated Lean community Zulip thread.
Bimonthly Community Meeting
The Community Meeting Google Meet is a bimonthly one-hour video call hosted by the Mathlib maintainers to discuss the present and future of Mathlib in Lean. Prior meeting recordings are available on the Lean FRO YouTube channel.