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.

At this month's Charleston Lean + AI Meetup, we'll discuss HILBERT: Recursively Building Formal Proofs with Informal Reasoning. The paper introduces a system that combines large language models with the Lean 4 proof assistant to automatically generate and verify mathematical proofs. We'll look at how HILBERT breaks complex problems into smaller subgoals and uses both informal reasoning and formal verification to solve them. The discussion will focus on what this approach means for improving AI-assisted theorem proving.