Mission.
NYC Lean brings people together to learn and use Lean 4, a programming language and proof assistant for writing verified software and checking mathematical proofs. We host free public talks, workshops, and working sessions in New York City where mathematicians, computer scientists, and students learn about Lean and its applications.
Our goals are to help newcomers learn Lean 4, to build a community among people who use Lean in New York City, to facilitate the exchange of ideas, and to make our talks and materials freely available to the public.
History.
NYC Lean began in May 2024 as an informal weekly meetup of people using Lean 4 in New York City, gathering in coffee shops, parks, and libraries. In August 2026 the organizers formed NYC Lean Group Inc., a New York nonprofit and 501(c)(3) charity, to support and grow that community. In September 2026 our meetups moved to NYU's Warren Weaver Hall.
Programs.
Weekly meetups. We meet every Sunday afternoon, currently at NYU's Warren Weaver Hall in Manhattan. Every event is free and open to the public. The schedule is on the calendar.
Public talks. Since June 2026 we have hosted researchers and engineers speaking on applications of Lean 4 to computer science:
- Verified differential privacy Markus de Medeiros
- Extracting verified programs to C++ Joomy Korkut
- Convergent replicated data types Alexander Städing
- A computer algebra system that proves its answers Jon Kleid
We have also hosted talks on applications to mathematics:
- The Gelfand–Naimark–Segal construction Gregory Wickham
- Gromov's theorem on groups of polynomial growth Aaron Hill
- The converse to the four-vertex theorem Kristoffer Josefsson
- Prove2Me, a collaborative platform for large-scale formalization Kunal Marwaha
Short write-ups of past talks are on the blog.
Going forward, we plan to organize hands-on beginner workshops that help newcomers learn the Lean programming language and proof assistant. We are also seeking funding to host larger events, such as workshops and conferences, that bring together researchers and corporations working on formal mathematics and verified software.
Get involved.
Interested in coming? Check the calendar for the next meetup, or say hello on the New York City thread of the Lean Zulip. To give a talk, email justin@lean.nyc.
Leadership.
NYC Lean Group Inc. is governed by a board of directors: Justin Asher (President), Kiran Gopinathan (Secretary), and Jack McCarthy (Treasurer). Loren Abdulezer also helps organize the community.
Organization details.
- Legal name
- NYC Lean Group Inc.
- Tax status
- 501(c)(3) public charity
- EIN (Charity ID)
- 42-4688495
- Incorporated
- August 17, 2026, New York
- NY Charities Reg. No.
- 51-78-56
- Address
- 160 Water St, Apt 26F
New York, NY 10038 - justin@lean.nyc
- Website
- lean.nyc
Contributions to NYC Lean Group Inc. are tax-deductible to the extent allowed by law. lean.nyc is the official website of NYC Lean Group Inc.