Short introduction video in Lean4

Stream: Lean for teaching

[Xavier Généreux]

Hi everyone,

I was wondering if there exists a video that could serve as a quick introduction to lean4 for students that have never been exposed to formalisation. Something that is more or less equivalent to this video in lean3.