Functional Programming & Theorem Proving in Lean

We’re launching a new series dedicated to verification and formal reasoning in Lean — centered around two excellent Lean resources:

• Functional Programming in Lean, a free Lean book that teaches writing programs in Lean’s pure functional language with proofs built in.
• Theorem Proving in Lean 4, a companion Lean book focused on interactive theorem proving and verifying properties using Lean tactics and dependent types.

Lean uniquely unites programming and proof, allowing you to write real code and formally verify its correctness. This series will help you explore that blend step by step.
In this session, we’ll:

• Get familiar with the structure and goals of both books.
• Walk through the beginnings of Functional Programming in Lean, including basic definitions, recursion, and simple proofs.
• Introduce key ideas from Theorem Proving in Lean 4 to support writing proofs about models and programs.
• Work on small Lean exercises together: writing definitions, proving simple properties, and sharing approaches.

Who it’s for:
Anyone curious about using Lean for software verification, algorithm correctness, or proof-driven development — whether you’re new to Lean or have some experience. Bring your laptop, a Lean environment (optional but helpful), and questions!
Let’s dive into Lean, mix programming and proof, and learn together how to build verified software with expressive dependent types.