Stream topic

Stream: mathlib4

[Joachim Breitner]

The topic of this stream still says “porting mathlib to lean 4”, but it’s too noisy for that to still be true, I think.
Also, the #maths stream says “maths / mathlib”, which I find a bit unclear. Is it (only) about the maths itself? Or about everything related to mathlib as well?
Assuming that mathlib-topics should not go into #general (is that true?), where do mathlib discussions go?

[Bolton Bailey]

Yeah I have been a bit confused these days as to which things should go in #mathlib4 and which in #general, definitely seems like it's not just "porting" here, so maybe we can come up with a better topic description.

[Scott Morrison]

Yes, it's certainly not about porting anymore.

[Scott Morrison]

I've just updated all the descriptions.

[Jon Eugster]

dump question, how do I see the full stream description? If I open the stream selection, I only see truncated "The main mathematics library for Lean. Discuss future changes and contr..."

[Scott Morrison]

My suggestion is:

• if it's about Lean 4 the programming language, it goes in lean4
• if it is about the current or future contents of Mathlib, it goes in mathlib4
• if it is about mathematics that could/should/would be formalized, but you need to think about some maths to do so, it goes in maths
• anything else goes in general

[Scott Morrison]

@Jon Eugster, can you click the three dot drop-down menu next to the stream name in the left bar, and then select "stream settings"? I can see the full description there.

[Damiano Testa]

(For me, it is an i inside a circle, rather than the 3 dots, on Android)