Zulip Chat Archive

Stream: Lean for the curious mathematician 2020

Topic: stream events

Notification Bot (May 13 2020 at 17:45):

Stream created by Jalex Stark.

Jalex Stark (May 13 2020 at 18:35):

Maybe this stream should be called Event planning : <title of event>?

Jalex Stark (May 13 2020 at 18:36):

I see it in my stream list underneath "Lean for teaching" and it doesn't seem to inspire the idea that it's about something specific

Jalex Stark (May 13 2020 at 18:36):

especially since the "2020" part of the title is cut off due to width

Reid Barton (May 13 2020 at 18:36):

wouldn't you see "Event planning: Lean ..." then? which gives no information

Jalex Stark (May 13 2020 at 18:37):

we could give it an abbreviation

Jalex Stark (May 13 2020 at 18:37):

LCM 2020 :P

Reid Barton (May 13 2020 at 18:37):

perhaps "Lean for teaching" can just be renamed to "Teaching"

Mario Carneiro (May 13 2020 at 18:37):

it's not a real conference unless it has an acronym

Reid Barton (May 13 2020 at 18:38):

I guess it's potentially ambiguous with "how to teach Lean" but I think that is okay

Reid Barton (May 13 2020 at 18:38):

Mario Carneiro said:

it's not a real conference unless it has an acronym

But wait, it's supposed to be for mathematicians...

Jalex Stark (May 13 2020 at 18:38):

"how to teach lean" is spontaneous conversations on "new members"?
I guess there's also "how to teach lean in the classroom" which happens on the "Lean for teaching" stream right now

Johan Commelin (May 13 2020 at 18:38):

We only have ICM

Mario Carneiro (May 13 2020 at 18:39):

which, ironically, was originally a stream intended for giving personal introductions

Reid Barton (May 13 2020 at 18:39):

I meant more like discussions on the books like Jasmin's and Mathematics in Lean

Jalex Stark (May 13 2020 at 18:39):

maybe we should have an introductions stream

Jalex Stark (May 13 2020 at 18:39):

the last time that people made introduction threads some value was generated

Jalex Stark (May 13 2020 at 18:39):

it'd be good if they were easy to find

Mario Carneiro (May 13 2020 at 18:39):

I'm saying, that's "new members"

Mario Carneiro (May 13 2020 at 18:40):

it came with the original zulip instance

Jalex Stark (May 13 2020 at 18:41):

sure, but maybe we should have a stream called "introductions"

Jalex Stark (May 13 2020 at 18:41):

where the only thing there are introduction threads

Jalex Stark (May 17 2020 at 14:07):

(I still think this stream could be profitably renamed to something like LCM 2020, though maybe that requires consensus among organizers about what acronym is appropriate)

Last updated: Dec 20 2023 at 11:08 UTC