Hacker Newsnew | past | comments | ask | show | jobs | submitlogin
Ask HN: Looking for a good course to learn proof assistant Lean 4
5 points by rabarbers 6 months ago | hide | past | favorite | 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!



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


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


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


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?




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: