Charleston Lean+AI Meetup

Lean is a functional programming language with a highly expressive type system. It can be used to produce performant programs that are guaranteed to meet their specifications, which proves that a large class of bugs cannot exist in your program. It can also be used to interactively prove theorems in mathematics. This meetup is for enthusiasts to join together to learn, code, and share their experiences with Lean.

The Lean+AI meetup is back! At our next meeting, we will dive into open-source AI systems that can support programming and proving in Lean. In particular we will start with Goedel-prover-V2, walking through installation, deployment, and exploring the model's capabilities with Lean. Join us to learn, experiment, and discuss where these tools can take us!