Lecture recordings

Stream: Lean for Scientists and Engineers 2024

[Tyler Josephson ⚛️]

Here's the Lecture 1 recording: https://umbc.webex.com/umbc/ldr.php?RCID=e91c7b67a5dbc8aab81c9175669068b2

[Tyler Josephson ⚛️]

Here's the Lecture 2 recording: https://umbc.webex.com/umbc/ldr.php?RCID=484469c27cc717724335ffc8c542549d

Expect the lecture slides and revised Lecture2.lean file tomorrow or Friday. I'm going to take some time to clean those up based on feedback during lecture.

[Simon Beaumont]

Might it be a good idea to create a git hub repo for the lean artefacts (and maybe lecture slides) for the course?

[Kevin Buzzard]

In all the informal courses I've given, I've set up a course repo on GitHub which depended on a fixed version of lean and mathlib, written down precise instructions on how to install it, added stuff later and encouraged people to pull, and then never bumped mathlib during the course because this can break people's setups. I also have a rule that once I've pushed a file, I never edit it, because I push files with exercises and students fill in the sorries, and if I change one of these files then the students who edited them get merge conflicts :-/ But sticking to these rules has led to good experiences on the student side.

[Nathaniel Budijono]

I don't seem to be able to see the chat from the recordings. Will the links to the survey be included somewhere? Perhaps the comments column of the schedule?

[Eric Taucher]

Kevin Buzzard said:

I've set up a course repo on GitHub which depended on a fixed version of lean and mathlib, written down precise instructions on how to install it, added stuff later and encouraged people to pull, and then never bumped mathlib during the course because this can break people's setups.

I took a look at your GitHub repositories (excluding forks) and while I think I found a few you noted, would be pleased if you could identify the ones you are thinking about in a reply.

As we know having a few examples help and for those doing this course you might have the needed info some may be looking for such as how to setup the project in VSCode, how to go from nothing to a working project in Lean, etc.

Thanks.

[Kevin Buzzard]

Sorry, I've been travelling (and still am, making my way home from Portugal). Formalising mathematics 2024 is an example (sorry no link, on mobile)

[Eric Taucher]

Kevin Buzzard said:

Formalising mathematics 2024

Thanks.

https://github.com/ImperialCollegeLondon/formalising-mathematics-2024

[Kevin Buzzard]

Yes that's a good example. That was the repo for a course which was run for lean beginners who were not computer scientists, so I spell out all the ways I know of using the repo. It has many files some of which import others so I didn't explain that you can just cut and paste a file into the lean web editor, but all the other methods should work with any repo. In my repo called something like IISCexperiments I even document in the README how I set up gitpod and codespaces but maybe you know how to do this already, and this repo is a year old so a lot has changed

[Kevin Buzzard]

During the course I would add more files and tell the students to "pull", and they seemed to be able to manage this.

[Tyler Josephson ⚛️]

Lecture 3 recording! https://umbc.webex.com/umbc/ldr.php?RCID=6be1e5636d1d1e42952bf1b073c53be0

Still prepping for the next one! If I catch up, I'll consolidate items on GitHub as suggested above, and also edit the recordings for YouTube.

[Dhruva Sambrani]

Tyler Josephson ⚛️ said:

Lecture 3 recording! https://umbc.webex.com/umbc/ldr.php?RCID=484469c27cc717724335ffc8c542549d

Still prepping for the next one! If I catch up, I'll consolidate items on GitHub as suggested above, and also edit the recordings for YouTube.

This seems like the link to lecture 2?

[Tyler Josephson ⚛️]

Oops! Here it is: https://umbc.webex.com/umbc/ldr.php?RCID=6be1e5636d1d1e42952bf1b073c53be0

[Tyler Josephson ⚛️]

Lecture 4 recording! https://umbc.webex.com/umbc/ldr.php?RCID=94c58c20d9de582087a0ae839c8f2903

[Eric Taucher]

Tyler Josephson ⚛️ said:

I'll consolidate items on GitHub as suggested above

Any updates?

Not sure if a Github repository was created and I missed the notification.

[Tyler Josephson ⚛️]

I haven’t had the bandwidth to do this yet, but when I do, I will update that here and elsewhere.

[Tyler Josephson ⚛️]

Lecture 5 recording! https://umbc.webex.com/umbc/ldr.php?RCID=ebffa8e475a29d30868ba78c0ff4e477

[Tyler Josephson ⚛️]

Lecture 6 recording! https://umbc.webex.com/umbc/ldr.php?RCID=589e20326023c8f254f781cb9d961194

[Tyler Josephson ⚛️]

Lecture 7 recording! https://umbc.webex.com/umbc/ldr.php?RCID=303f1f86ec0bdc0cdfa675683bb5a6ca

[Tyler Josephson ⚛️]

Lecture 8 recording! https://umbc.webex.com/umbc/ldr.php?RCID=256a905852ce8c9b2552ed7697fc4b3f

[veysel]

No lecture for today?

[Tyler Josephson ⚛️]

Yep! Lecture starting now. Forgot to share slides and code.

[Tyler Josephson ⚛️]

Lecture 9 recording! https://umbc.webex.com/umbc/ldr.php?RCID=ffa9f673da7d5f51c0845178bb502220

[Tyler Josephson ⚛️]

FYI - as mentioned in class, via email, and Google Calendar, we will NOT be having class tomorrow. We continue next week.

[Tyler Josephson ⚛️]

Lecture 10 recording! https://umbc.webex.com/umbc/ldr.php?RCID=fe9a35f2373d174b78c08a44745abde2

[Tyler Josephson ⚛️]

Lecture 11 recording! https://umbc.webex.com/umbc/ldr.php?RCID=fdb070fac47f174fcecf60a96960eacc

[Tyler Josephson ⚛️]

And that's a wrap! Thanks to everyone who participated! I'm excited to see what y'all build moving forward.

[Somo S.]

@Tyler Josephson ⚛️ will you consider putting up these video recordings on youtube? The youtube video player has much more user friendly features for getting through long form content (e.g. x2 or x1.5 speed or double tap to skip 10seconds)

[Tyler Josephson ⚛️]

@Somo S. Yep! I had a student converting these videos over the semester, and he just finished the task. I’ll let you know here once I start getting them uploaded.

[Tyler Josephson ⚛️]

(I’m traveling for a few more days, and the flash drive is back home)

[Somo S.]

awesome look forward to seeing them

[Tyler Josephson ⚛️]

Now on YouTube! First lecture is here (more to come as I get them up): https://www.youtube.com/watch?v=s9Dyiu4S4vA
Playlist is here: https://www.youtube.com/playlist?list=PLX21uJ4UfpF43NExUcPcAEgnzV58x_26l