Splitting lean4?

Stream: Zulip meta

[Scott Morrison]

I wonder if it is reaching the point we should have multiple lean4 streams. My thinking is basically we should have "stuff Leo might want to see" and "stuff he won't". Zulip maintainers can then try to shuffle things into the right places at first.

[Mario Carneiro]

I don't think it's worth it at this time. The issue seems to be a mismatch of expectation regarding the level of formality on zulip in general, and I don't think we should make a split along formality lines because an #off-topic stream is sure to draw more off-topic things than we already get. I don't think we need to change anything regarding the level of jokes / code of conduct stuff either.

[Scott Morrison]

I was thinking more in terms of splitting into lean4-getting-started, lean4-general, and lean4-issues.

[Kevin Buzzard]

Oh that might be worth a try