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.

Lean4+AI Meetup – Proof Hacking Session

Join us for this month's Lean+AI meetup! AI progress has accelerated rapidly in recent months, and we're now at a point where mainstream systems like Claude Code and OpenAI Codex can meaningfully assist with Lean4 development.

For this session, we're following a hackathon-style format where participants explore a formalization of their choice, either solo or in groups. The goal is to spark discussion, experimentation, and collaboration. Think about what computer program, mathematical theory, or physical theory you'd like to formally verify, and let's see how far we can get together.

Bring your laptop, high-quality tokens, and your proof-hacking spirit!