Zulip Chat Archive

Stream: new members

Topic: Lean files of lftcm 2022


Jean-Marie Mirebeau (Oct 06 2022 at 16:43):

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 (Oct 06 2022 at 16:58):

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

Patrick Massot (Oct 06 2022 at 19:27):

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 (Oct 06 2022 at 20:47):

Thanks for the links. Exciting projects !


Last updated: Dec 20 2023 at 11:08 UTC