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!

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?

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