Lean working group in Toulouse

UPDATE: we have a website!

Together with my PhD student Aabhas Gulati, we’re excited to announce the launch of a new working group dedicated to exploring the formal proof assistant Lean. For a taste of why formalizing proofs is becoming so important, check out this video by Kevin Buzzard.

Our Plan:

• Goal: Master the basics of Lean and eventually embark on a project to formalize a result from your favorite area.
• Meetings: Every Friday at 2 pm, starting March 7th.

First Session Highlights:

• Meet and greet: Introduce ourselves and share our interests.
• Hands-on setup: Get Lean installed and running on your computer.
• Exploring tutorials: We’ll review resources like this or this.
• Plan our future sessions and potential collaborative projects.

No matter your background or previous experience with formal proofs, everyone is welcome. If you’d like to join this adventure, please reply to this message by February 28th so we can book an appropriate room. Feel free to reach out with any questions or suggestions and share this message with anyone in Toulouse that might be interested in joining!