BFPG Meetup - November 2026 - Lean

Join the BFPG Discord: https://discord.gg/yYz2d8w7FY

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.