Yury Kudryashov lecture in the Rutgers Lean seminar

Stream: general

[Newell Jensen]

Will the video be made available on YouTube afterwards?

[Alex Kontorovich]

Sure, we can try recording it and posting online. (If Yury agrees)

[David Renshaw]

Hey, I'm interested in watching this talk! Would anyone be willing to DM me the zoom link? (I tried DM'ing Alex a few minutes ago, but I suspect he's busy.) EDIT: Alex DM'ed me the link

[Newell Jensen]

I am also interested if someone could DM it to me as well. Thanks!

[Notification Bot]

4 messages were moved here from #announce > Yury Kudryashov lecture in the Rutgers Lean seminar by Johan Commelin.

[chenjulang]

Me too...

[Alex Kontorovich]

For those interested in the video of Yury's lecture, it is available here:

https://rutgers.zoom.us/rec/share/5ahPR4Jzl1a36whPFkYtZHs3OGmku4jdczP-dQ2D8qvSmq8KexsM4n1jqzoB86rY.aM_G43Cdr_tJKBau

Password: R!9&w?Cy

And his slides are attached.
mathlib-holes.pdf

[Kevin Buzzard]

The beamer handout setting (I think it's called that) would make the slides much easier to read -- right now there are 123 slides and lots of repetition.

[Mauricio Collares]

mathlib-holes-handout.pdf

[Junyan Xu]

image.png
This is now done in #10327