Hi HN,
I’ve been exploring Lean 4, the theorem prover and programming language, and I’m impressed by what it offers for formal reasoning and proofs. However, it’s been difficult to find a structured, instructor-led course or organized study group (as opposed to just tutorials or documentation).
Does anyone know of:
University or online courses (open enrollment) teaching Lean 4
Any guided cohorts, bootcamps, or community study programs.
My goal is to learn Lean 4 in a more systematic and interactive way — ideally with feedback, projects, or peer discussion.
If you’ve taken such a course, organized one, or know where to look (e.g. Discords, Zulip groups, or university links), I’d love your pointers.
Thanks!
The 2025 edition material is at https://github.com/lean-forward/logical_verification_2025?ta...
An older version (2022-2023) with video lectures is at https://lean-forward.github.io/logical-verification/2022/ind...
Ignoring that advertised case a few years ago, what are non-trivial theorems that you can prove with it?