lean-mode

A reading club working through Theorem Proving in Lean 4 (Avigad, de Moura, Kong, Ullrich) with an applied component where we implement the exercises and discuss them together.

Who is this for

Peers curious about Lean, formal verification, or theorem proving. No prior Lean experience required, but comfort with programming and basic logic helps.

How it works

• We meet weekly on Monday at 7pm UTC
• Each session covers a chapter or subset of chapter, depending on chapter complexity
• Format: one person presents key concepts, then we walk through exercises together
• Between sessions: read the chapter, attempt the exercises, push your solutions to your own fork

Joining

Discord invite link

Set up

Installation Guide

Repo structure

• session-XXX/: notes & exercise solutions, one folder per session

Current progress

We're on Chapter 2. Next session: 25 May 2026 (2.8-2.9)