lean.zulipchat.com

Stream: Zulip meta

[Kevin Buzzard]

I am a bit unsure what to make of this. Someone I know just attempted to create an account on "the Lean Zulip", got a message saying that it was not possible without being invited, and then emailed me and asked if I'd invite them. I told them that an invitation was definitely not necessary, and it transpired that they had gone to lean.zulipchat.com as opposed to this Zulip, which is leanprover.zulipchat.com . Is the other Zulip instance (a) some kind of attempt to confuse people looking for the Lean Zulip (b) some genuine thing, perhaps associated to some other use of the word "lean" (c) a defunct attempt by our community to set up a Zulip instance (which could then perhaps be removed) or (d) something else?

[Matthew Ballard]

FRO?

[Jireh Loreaux]

"the coolest place in the universe" doesn't seem like something the FRO would write?

[Matthew Ballard]

I think that is the default

[Kevin Buzzard]

I think that was also our tagline for quite some time, I had assumed it was just Sebastian Ullrich's sense of humour back in 2018 but then I realised that actually there were a ton of zulips with the same comment

[Sebastian Ullrich]

Matthew Ballard said:

FRO?

No

[Matthew Ballard]

There is also that other lean

[Kunal Marwaha]

"the coolest place in the universe" seems like a Zulip default for many years: https://github.com/zulip/zulip/blob/3e54ae9f4d5c1086b7a760be2909010b70ebdaec/zerver/lib/realm_description.py#L13

[Alex Vandiver]

lean.zulipchat.com was very very inactive, and not set up by anyone related to this Zulip instance. I've set it up to redirect to here.