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

5 points by rabarbers a day ago

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!

aborsy 5 hours 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?