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
The Lean FRO and community members host several regular meetings. The aggregate events calendar below includes all listed events.
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 Mathlib Community Meetings
The Mathlib 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.
The Meta Café
The Meta Café Google Meet is a community meeting organized by the Mathlib Initiative to discuss developments in Lean's tactic and meta-programming ecosystem.
Weekly CSLib Meeting
The CSLib Meeting Google Meet is a weekly video call for contributors to and users of CSLib, a foundation for Computer Science in Lean, to discuss development and planning. Prior meetings recordings are available on the Lean FRO YouTube channel.