Zulip Chat Archive

Stream: Lean Together 2021

Topic: Automatically generalising theorems using typeclasses


view this post on Zulip 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/ .

view this post on Zulip Gabriel Ebner (Jan 06 2021 at 14:54):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jan 06 2021 at 15:03):

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

view this post on Zulip 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.

view this post on Zulip matt rice (Jan 06 2021 at 15:05):

or is it topology MySpace

view this post on Zulip Johan Commelin (Jan 06 2021 at 15:06):

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

view this post on Zulip Johan Commelin (Jan 06 2021 at 15:09):

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

view this post on Zulip Johan Commelin (Jan 06 2021 at 15:24):

"it's quite fond of silicon scrap sometimes"

view this post on Zulip 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: May 08 2021 at 22:13 UTC