Lean 4 university course lectures?

Stream: new members

[Isak Colboubrani]

I am compiling a list of Lean 4 video lectures from university courses for mathematics and computer science students.

Currently, I have found Brown University's CS 1951x: Formal Proof and Verification (Fall 2023), with 22 out of 24 lectures available at https://browncs1951x.github.io.

Are there other universities offering public access to Lean 4 course lectures?

[Patrick Massot]

Do you know the list from https://leanprover-community.github.io/teaching/courses.html? Note it has nothing specific to video recordings.

[Isak Colboubrani]

@Patrick Massot Yes, I have reviewed all the courses, and it appears that Brown University's CS 1951x is the sole university-level Lean 4 course in English on that list which offers publicly accessible video recordings.

[Max Nowak 🐉]

There is also https://github.com/IPDSnelting/tba-2022

[Isak Colboubrani]

@Max Nowak 🐉 I reviewed the course but was unable to locate any video lectures. Could you please confirm if they are available to the public?

[Max Nowak 🐉]

Ahhh apologies I failed to read “video”. I don’t think these were recorded unfortunately

[Martin Dvořák]

I will be giving a short Lean tutorial (3 two-hour-long classes on 2024-02-06, 2024-02-07, 2024-02-08) at Institute of Science and Technology Austria that will be recorded. However, it will be a very small tutorial for Ph.D. students in Computer Science, most of which already publish research in formal methods. It is far from what would satisfy the criteria for university courses.

[Isak Colboubrani]

@Martin Dvořák Great! A PhD-level mini-course with recorded lectures would perfectly meet the criteria I'm looking for. I'm eager to add it to my list once it becomes available.

[Isak Colboubrani]

@Martin Dvořák Please inform me if or when the video lectures become available. I'm eagerly looking forward to watching them!

[Martin Dvořák]

I am sorry; there will be no recordings. We ended up only streaming them, not recording.