Local/city threads

Stream: new members

[Orpheus Lummis]

It seems useful to have threads supporting in-person interactions for specific localities or cities. E.g. I'd like to create a thread for Montréal. Where should such threads exist?

[Orpheus Lummis]

An idea is to have a new stream, perhaps named 'local', under which they would exist

[Johan Commelin]

I think that in principal you could even create a new stream "Montéal Lean User Group". I think there are such streams for IC London, and for ALU Canberra.

[Rob Lewis]

Those streams are private, I think, so they serve a different purpose.

[Rob Lewis]

I'm not sure we have the userbase to justify threads for lots of cities, but on the other hand, there's not much cost to a new stream.

[Kevin Buzzard]

There is a private Imperial stream, and it's for Imperial students who basically might be too scared to ask their simple questions on the "real" chat; there are also local conversations which go on there such as when Xena starts/stops etc.

[Bhavik Mehta]

There is a private Imperial stream, and it's for Imperial students who basically might be too scared to ask their simple questions on the "real" chat; there are also local conversations which go on there such as when Xena starts/stops etc.

There's a similar one for Cambridge as well

[Reid Barton]

As a general rule, streams are the mechanism for people to select what messages they want to see. You can be subscribed or not to each stream, but you can't really be subscribed or not to a topic (there is topic muting which is sort of similar, but doesn't make sense for a case like this). So one stream per city is logical.

[Mathieu Guay-Paquet]

It seems useful to have threads supporting in-person interactions for specific localities or cities. E.g. I'd like to create a thread for Montréal. Where should such threads exist?

Hey, I'm in Montreal too, and fairly new to Lean! I'd love to have in-person interactions

[Luis O'Shea]

I’m in NYC and would also love to meet up with Lean enthusiasts

[Jalex Stark]

I made a stream called "Geographic locality" with the following mechanism in mind:
anyone can visit and see if there is a topic about their city. If so, that topic has pointers to other people in their city / a private stream / a regular meetup. If not, they could make a topic about their city and hope that this eventually leads to someone else poking them

[Mario Carneiro]

That also sounds like a good place for threads about (the physical logistics of) conferences