Online coursers or any possible set of lectures

Stream: new members

[Plamen Dimitrov]

Hi all, does anyone know if there is a good comprehensive course in Lean 4 online or in any uni you could recommend? Video or live lectures would be great to get more personal with the overall ideas behind this language. And yes, I have already read big parts of the https://lean-lang.org/theorem_proving_in_lean4 and small parts of https://lean-lang.org/doc/reference/latest.

[Kevin Buzzard]

I don't have an answer but are you looking for a more mathematical or more CS introduction?

[Plamen Dimitrov]

I have already taken some lectures in type theory as well as proof theory so the emphasis I would love to see would be strictly on using and completing proofs with Lean 4 - even hands-on workshop with the language would be really nice to have.

[Kevin Buzzard]

Yes but do you want to see proofs about lists and types and arays or about topological vector spaces and schemes?

[Plamen Dimitrov]

I think the topological vector spaces are rather a more advanced topic here related to homotopy type theory. I am fine seeing proofs about lists, natural numbers, and hopefully involving at least some type classes (e.g. from order theory ) in order to get a the overall feel about the language. Of course I am aware the choice is likely not going to be particularly large so any kind of lectures or workshops involving Lean 4 would be welcome.

[Plamen Dimitrov]

I assume no one has any ideas / suggestions?

[Niels Voss]

I think you might be interested in #mil, which gets you doing actual math in Lean as fast as possible. The other major learning resource is #tpil, which is more type theory oriented. Based on what you said above, I think Mathematics in Lean is a better choice, but you should use Theorem Proving in Lean 4 as a reference.

[Niels Voss]

Oh wait, sorry, I didn't read your question close enough. I didn't realize you requested video lectures specifically and had already looked at Theorem Proving in Lean 4

[Kevin Buzzard]

Making a good comprehensive online course costs a lot of time and money, so the chances of it existing right now is low because the community is quite new and small (at least in comparison to the big programming langauges), and Lean courses do exist but they typically run in universities rather than online. The chances of a good comprehensive course existing in the part of the ecosystem which you are speficically interested in is I guess even lower. You should perhaps take a look at https://leanprover-community.github.io/teaching/index.html and contact anyone directly if it turns out that they've run a course in the part of the ecosystem which you're interested in, to see what resources they have. For example all the documentation for Imperial's Lean course (which is more math-focussed and AFAIK doesn't mention lists once) is here and here, but I'm afraid there are no publically-available videos (to access the videos you need to be registered for the course).

[Plamen Dimitrov]

Niels Voss said:

Oh wait, sorry, I didn't read your question close enough. I didn't realize you requested video lectures specifically

Nevertheless, these are great read-up alternatives so thanks for that!

Kevin Buzzard said:

You should perhaps take a look at https://leanprover-community.github.io/teaching/index.html

This is also a great reference for previously existing courses and universities / people that actually teach Lean 4 directly or indirectly, will take a look as well! I guess then video courses are too much to ask given the current stage and scope of the community but I am glad to see there are at least some reading-based alternatives.