Lean files of lftcm 2022

Stream: new members

[Jean-Marie Mirebeau]

Hello,

In the videos of lftcm 2022 conference, which are available online, several speakers illustrate their talk by interactively completing some lean files. However, I cannot find these on the lftcm 2022 website, or anywhere online.
https://icerm.brown.edu/topical_workshops/tw-22-lean/

Were such files distributed to the participants, and if that is the case could they be made available online ?

I ask this question because there is a repo containing the lean files of the earlier lftcm 2020 conference, which proved to be an excellent learning material.
https://github.com/leanprover-community/lftcm2020

[Johan Commelin]

I think most files were posted in the zulip stream #LftCM22

[Patrick Massot]

Hi Jean-Marie! It's great that you are interested in Lean. We really need more people from applied mathematics. As you can see by comparing https://leanprover-community.github.io/undergrad.html and https://leanprover-community.github.io/undergrad_todo.html we are doing a really bad job of formalizing even very basic numerical analysis. And Lean 4 will allow even nicer things in this direction, see https://github.com/lecopivo/SciLean for a glimpse of the future.

[Jean-Marie Mirebeau]

Thanks for the links. Exciting projects !