Ask HN: Looking for a good course to learn proof assistant Lean 4

5 pointsby rabarbersقبل 8 أشهر4 comments

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!

4 comments

gkuقبل 8 أشهر

CS 99: Functional Programming and Theorem Proving in Lean 4,designed by Stanford University Centaur Lab: https://web.stanford.edu/class/cs99/

i_don_t_knowقبل 8 أشهر

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...

hctaقبل 8 أشهر

I located this course https://github.com/ATOMSLab/LFSE2024 with video lectures @ https://www.youtube.com/@tylerjosephson8860 . Let us know if it's good

aborsyقبل 8 أشهر

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?