Hello! We’re a friendly group of Lean enthusiasts who meet weekly for a talk or presentation, followed by discussion, hands-on learning, and group projects.
Our members include researchers, industry professionals, students, startup founders, consultants, curious community members — and hopefully YOU!
One of the great things about Lean is that it attracts people from many disciplines: math, CS theory, AI, software engineering, cryptography, physics, and economics, to name a few. Our members come from all of these backgrounds, and we welcome others with any level of experience, including first timers.
While Lean is our focus, don’t be surprised if you get pulled into conversations about programming languages, formal methods, or AI-assisted coding.
When: Monday evenings at 7pm. Sessions run 1–2 hours, with the “official” portion lasting about an hour.
Where: Mox SF (1680 Mission St, San Francisco)
Luma has more information about upcoming talks and events.
Join the Discord to stay up to date on events and discussions — concatenate https://discord.gg/ and bXNPh and Qyjfe and paste into your browser. All our communication happens on Discord.
If you have time before you arrive, try installing the Natural Number Game locally. You’ll want to open the repo in a VSCode devcontainer and open http://localhost:3000 in your browser.
If you’d like to skip straight to the math, clone Terence Tao’s repo:
git clone https://github.com/teorth/analysiscd analysis/analysislake exe cache getSection_2_2.lean and filling out the sorrys.Good luck! You can ask for help in the Discord server.