Zulip Chat Archive

Stream: LftCM22

Topic: stream events

Notification Bot (Jul 11 2022 at 01:52):

Public stream created by Johan Commelin. Description:

Lean for the Curious Mathematician (ICERM 2022)

Johan Commelin (Jul 11 2022 at 13:08):

Welcome everyone to this stream for the workshop "Lean for the Curious Mathematician 2022" at ICERM. Feel free to discuss anything Lean/workshop related in this stream.

Heather Macbeth (Jul 11 2022 at 14:04):

Hi everyone! And hi to our virtual participants in particular.

Just in case you're worried (we had a few questions), the next talk, by Kevin Buzzard, will not require Lean to be installed on your machine. You'll interact with Lean over the internet.

Heather Macbeth (Jul 11 2022 at 14:06):

We have a dedicated installation session scheduled at the end of today, but feel free to reach out here for help if you try it before then and get stuck. Here are basic instructions:
https://leanprover-community.github.io/get_started.html

The first time you will need a Lean installation is tomorrow morning.

Heather Macbeth (Jul 11 2022 at 19:28):

The session on installation help will be pretty informal. But it will officially start 15 minutes late, at 3:45.

Last updated: Dec 20 2023 at 11:08 UTC