Wednesday morning

Stream: Lean for the curious mathematician 2020

[Johan Commelin]

Hello everyone, the first session will start in 15 minutes.

The first speaker of today is Floris van Doorn, and he will explain about "structures and classes". Because it is currently in the middle of the night at his side of the earth, Floris has kindly pre-recorded two videos.

Please watch the first video, and then join the breakout rooms. Halfway through the session, we will send a broadcast message, to remind everyone to start watching the second video.

The videos are available at https://www.youtube.com/playlist?list=PLlF-CfQhukNloaV_NiVvgJt-Pr6lQd56q .

If you have any questions about the content of the videos, please ask the tutor in your breakout room!

[Johan Commelin]

If you've finished watching the first video, please go to Zoom, and we'll assign you a breakout room.

[Johan Commelin]

So far, we've started three breakout rooms.

[Johan Commelin]

If you are ready to enter a breakout room, please tell me.

[Dima Pasechnik]

Which Zoom session to go to? Could you post the link etc?

[Johan Commelin]

@Dima Pasechnik Zoom details are here: https://leanprover.zulipchat.com/#narrow/stream/238830-Lean-for.20the.20curious.20mathematician.202020/topic/Zoom/near/203928237

[Johan Commelin]

Join Zoom Meeting
https://vu-live.zoom.us/j/95402085900

Meeting ID: 954 0208 5900
Password: 333537

[Johan Commelin]

@ everyone, if you have finished watching the first video. Please join Zoom, and ask me to assign you to a breakout room.