Zulip Chat Archive

Stream: Lean Together 2021

Topic: Automatically generalising theorems using typeclasses

Alex J. Best (Jan 06 2021 at 14:51):

Hi everyone, I've just uploaded my asynchronous talk to
https://bostonu.zoom.us/rec/play/JTataWlqYtJoB2AT0fI2kkHQMgFT6eHSS6jnwXPbWq0R4yspbGWi19DoUrik-Nz-tauQTETTj7jD3jE-.BS4XYryhlgrHECTm?autoplay=true
During the later social hour tomorrow evening (at the end of the conference) will be the scheduled discussion session for the talk in gather, where we can chat about it.
So if you are interested and have a chance to watch it before then (~35mins) I'd love to hear your feedback and questions!
The slides are at http://alexjbest.github.io/talks/lean-generalisation/ .

Gabriel Ebner (Jan 06 2021 at 14:54):

In case anybody else is wondering where the slides are, you need to press PgDown.

Alex J. Best (Jan 06 2021 at 14:56):

Oops, yes thanks Gabriel, I press left and right on my keyboard (I didn't use the fancy navigation in 2-dimensions feature!), https://alexjbest.github.io/talks/lean-generalisation/?print-pdf#/ is a more scrollable / printable link to the same

Johan Commelin (Jan 06 2021 at 14:58):

The transcription is hilarious at times!!

Alex: Let RR be a commutative ring.
Otter.ai: Let I'll be it can be different.

Johan Commelin (Jan 06 2021 at 15:03):

We don't want to end up with duplicated plumbers in math lab (-;

Heather Macbeth (Jan 06 2021 at 15:04):

Alex: So, this lemma, it's about finsets and you've got the linear ordered field.
AI: So Islam or it's about fan sets and you for the linear audit field.

matt rice (Jan 06 2021 at 15:05):

or is it topology MySpace

Johan Commelin (Jan 06 2021 at 15:06):

Linda is quite smart. I'm really glad she's helping us improve mathlib!

Johan Commelin (Jan 06 2021 at 15:09):

GPT 4 is going to be trained on the transcripts of these videos :see_no_evil:

Johan Commelin (Jan 06 2021 at 15:24):

"it's quite fond of silicon scrap sometimes"

Kevin Buzzard (Jan 06 2021 at 17:24):

I recorded a bunch of videos in Sept and they were all auto-captioned, and it took me longer to fix up the auto-captioning than it did to make the videos. https://twitter.com/XenaProject/status/1313859808387362818?s=20

Last updated: Dec 20 2023 at 11:08 UTC