Ask HN: Looking for a good course to learn proof assistant Lean 4
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!
I have been eyeing “The Hitchhiker's Guide to Logical Verification” but haven’t yet found the time to work through it.
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...
What can you prove with it?
Ignoring that advertised case a few years ago, what are non-trivial theorems that you can prove with it?
I located this course https://github.com/ATOMSLab/LFSE2024 with video lectures @ https://www.youtube.com/@tylerjosephson8860 . Let us know if it's good