Looking for Lean 4 courses or structured learning programs

Stream: new members

[Mikus Vanags]

Hi everyone!
I’ve been learning Lean 4 through the available tutorials and Theorem Proving in Lean 4 book, but I’m interested in finding a more structured or guided way to learn — ideally an online course, university offering, or cohort-style program that I could join.
Does anyone know of:
Current or upcoming Lean 4 courses (open enrollment or academic)
Any study groups, bootcamps, or guided learning initiatives
Or other structured programs where I could apply and learn interactively
Self-paced resources are great, but I’d really like to follow a clear curriculum and get feedback or discuss with peers.
Thanks a lot for any pointers or links!

[Kevin Buzzard]

What's your background? Professor of mathematics? Computer science undergraduate? Your question is unanswerable right now. What do you want to learn?

[Michael Rothgang]

Do you want to understand how Lean works under the hood, in detail? Do you want to learn how to use Lean? For math proofs, software verification or as a programming language? Help us help you :-)

[Mikus Vanags]

Thanks for the reply!

I have a PhD in Information Technologies and work professionally as a .NET developer. I recently received funding for my postdoctoral project, “KatLang: Enhancing a Higher-Order Domain-Specific Language for Problem Solving and Educational Assessment in Mathematics and Physics.”

The goal is to advance the concept behind KatLang https://katlang.org and build web tools that let users define math and physics tests whose evaluation can be automated. The project officially starts on March 1, 2026.

My PhD research focused on abstractions in functional and logic programming (thesis: https://1drv.ms/w/c/d7aa8d71b9867c20/ESB8hrlxjaoggNfkBAAAAAABJqSJLk2MOsjl_L-eykn5dg?e=m49ryj ).

Even with that background, I’ve found proof assistants quite challenging to grasp. So far, my best progress has been working through the https://adam.math.hhu.de/#/g/leanprover-community/nng4 , but I still feel like I understand almost nothing.

My main goal with Lean 4 is to explore how to formally describe KatLang’s semantics and properties, and to see what theoretical insights we can derive from that. Conceptually, I think of KatLang as a way of decomposing the lambda abstraction and reassembling it into something more expressive—a kind of “mathematical algorithm” abstraction that can combine several functions rather than just return a single value.

Over the past few days, I’ve been searching for Lean 4 online courses I could apply to, but haven’t had much luck yet. If anyone knows of opportunities—or is interested in collaboration - I’d be very happy to connect.

I’d love to understand how Lean really works inside, but I’m not there yet.

[CY Fung]

Hi Mikus, I am looking for people who are interested to learn Lean together. See

#new members > New to Lean; Wanna form a small study group @ 💬

[Yan Yablonovskiy 🇺🇦]

There is a list here if you didnt know yet.