Charleston Lean Proof Assistant 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.

For our second meeting, we will build up the natural numbers (the unbounded, non-negative integers) from scratch and prove basic facts about them. Building these numbers from scratch will let us use the tools that Lean provides for constructing data structures. We can then define addition and multiplication from first principles, and prove that x+y is equal to y+x. Time permitting, we could show how we could then go about defining the rational numbers, and build out a robust library for arithmetic.