Welcome to Stanford Lean Club
Introducing our new club dedicated to the formalization of mathematics in Lean.
We are excited to announce the launch of the Stanford Lean Club!
Our Mission
Our goal is to bring together students and researchers interested in:
- Formal Verification: Using tools like Lean 4 to mathematically prove the correctness of software and theorems.
- Formalization of Mathematics: Contributing to Mathlib and formalizing modern mathematics in Lean.
- Education: Teaching the next generation of mathematicians and computer scientists how to use these powerful tools.
Why Lean?
Lean is a functional programming language and theorem prover. It allows us to write mathematical definitions and theorems, and then prove them with the help of the computer. This ensures absolute correctness and opens up new possibilities for collaboration and automation.
Get Involved
We host weekly meetings, workshops, and hackathons. Whether you're a seasoned Lean user or just curious about the future of math, we'd love to have you join us!