Readit News logoReadit News
Posted by u/rabarbers a month ago
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!

gku · 24 days ago
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 · a month ago
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 · a month ago
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 · a month ago
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?