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

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?

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

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

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