What is #mathlib4 about now?

Stream: new members

[Pedro Sánchez Terraf]

The description of #mathlib4 states “Porting mathlib to Lean4”. Is that still the case? Or is that stream being used for another purpose?

I have seen new replies to old topics, but there are also fresh topics as well.

Thanks in advance for the info! Trying to set reading priorities :sweat_smile:

[Tomas Skrivan]

The other day I was also thinking what is the point of #lean4 now, should it be merged with #general ? How do I decide where do I post.

[Anatole Dedecker]

No clear decision has been made about this yet and it's true that it's sometimes a bit confusing. Personally, I would post in #mathlib4 for topics at least loosely related to the switch to Lean4, even if that's not directly related to the port in itself (typically: performance issues, naming conventions, coordination with other Lean4 projects). Otherwise I just used the usual streams.

[Kevin Buzzard]

Yeah I've moved back to #general for the sort of questions which were going in #general before lean 4

[Jireh Loreaux]

I think having a #mathlib4 stream (perhaps without the 4) is useful. There are certain things which really are specific to mathlib, and it would be good if we weren't spamming the general stream with those.

[Jireh Loreaux]

I think even #lean4 (possibly renamed?) is useful. It can be a place for more functional programming concerns, and then #general can be for the overlap.

[Jireh Loreaux]

(Aside: is it possible to @ mention everyone subscribed to a particular stream, and only those people? Maybe only maintainers, or is this impossible? I have sometimes found myself wanting to draw the attention of people involved in mathlib to some topic, but not spamming everybody. Obviously if this exists it should only be used sparingly.)

[Mario Carneiro]

@ all

[Jireh Loreaux]

Ah, I didn't realize that wouldn't ping people that are unsubscribed, but that makes sense.

[Ioannis Konstantoulas]

I have been treating #lean4 as the place to ask questions about bare Lean 4, usually about programming, but also about theorem proving without any libraries. I would view #mathlib4 as a place to discuss strengths and weaknesses of mathlib: performance, readability, documentation, structure, future modules, refactoring concerns etc.

[Pedro Sánchez Terraf]

Jireh Loreaux said:

I think having a #mathlib4 stream (perhaps without the 4) is useful. There are certain things which really are specific to mathlib, and it would be good if we weren't spamming the general stream with those.

But now #maths is described as “mathlib / maths”, then it seems that place would encompass that :thinking:

[Jireh Loreaux]

That's not currently how we use #maths. I think for the most part we use that for discussing actual (often high-level) mathematical topics.

[Johan Commelin]

There's also @stream

[Bulhwi Cha]

Maybe we should change the descriptions of those streams.