BFPG Meetup - November 2026 - Lean
Join the BFPG Discord: Join Discord Server
Agenda
18:00: Welcome and setup
Presentation #1: Lean is a general-purpose functional programming language!? by Carlo Hamalainen
20:00ish: Pack down, head to Criterion pub
Lean is a general-purpose functional programming language?
Lean is best known as a theorem prover. Mathematicians use it to check proofs, and language models have recently been using it to produce whole formalisations on their own. But Lean 4 is also a strict, pure functional programming language with type classes, do notation, mutable-looking loops that desugar to pure code, and an ecosystem you can build a web server with.
We’ll briefly survey the landscape of theorem proving and LLMs, then look at some real-world examples of the “normal” code you’d write in Go or Python. Then we’ll pick up where George Wilson’s earlier BFPG talk on monoids left off: in Lean, the monoid laws can be fields of the class, so a dodgy instance won’t compile. We’ll prove those laws step by step, live in Lean.