lean discord server

Stream: general

[crab]

is there a lean discord server, or only zulip?

[Kevin Buzzard]

What's your background?

[crab]

background in what?

[Arthur Paulino]

crab said:

background in what?

He's asking about your academic background (grad mathematician, undergrad computer scientist etc)

[crab]

Arthur Paulino said:

crab said:

background in what?

He's asking about your academic background (grad mathematician, undergrad computer scientist etc)

then sudent

[Arthur Paulino]

I suspect he wants you to be a bit more specific :smiley:
Are you more familiar with programming or math abstractions?

[crab]

I use F# and rust. not really Math Abstractions, just number theory

[Arthur Paulino]

Oh, you had started a thread on this subject before:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/lean.20discord.20server/near/266735828

[Eric Wieser]

(I combined the threads)

[crab]

Oof

[crab]

I just really want a lean discord server

[Eric Wieser]

If you answer Kevin's question then you might get an invite to one

[Arthur Paulino]

@crab are you in high school? Is this what you meant by "student"?

[Kevin Buzzard]

I run a private discord server where I manage a bunch of undergraduate mathematicians. We're doing a course right now in London and I use it to run office hours and stuff. It's really mostly a "UK lean maths discord"; most people there are at Imperial or Cambridge. Maybe you should make a public lean discord if you want one? I just don't want to be involved in the management of it. My children have given me horror stories of when discord goes wrong so I don't want to open it up

[Kevin Buzzard]

I would happily do the advertising for you

[Kevin Buzzard]

I just don't want to be blamed if it gets nasty for some reason

[crab]

Kevin Buzzard said:

I just don't want to be blamed if it gets nasty for some reason

I would gladly make one, but there is a problem. I don’t really know lean well. It would be ironic if I ran a lean discord server, and I don’t even know lean

[Arthur Paulino]

@crab what do you think the Zulip chat is missing?

[crab]

It’s not what I’m used to

[Arthur Paulino]

Oh then it's just the tool itself? I'm usually more comfortable with Discord too and I use it for gamedev/pixel art groups. However, I find it rather distracting and thus not very suitable for the professional level that the Lean community needs

[Kevin Buzzard]

Discord couldn't compete with this place. The reason I run the maths discord is precisely because there are young mathematicians who want to informally play with lean and think this place is a bit intimidating (and also because my formalising club got shut down when the pandemic happened). This place is a serious research forum and I very much hope we keep it that way for as long as possible, with very few "trivial"' threads and a focus on high-quality discourse and problem-solving. The Xena discord is anything but this.

[Alistair Tucker]

Kevin has explained how we got here, but it does seem a little counterintuitive that the "informal play space" is a walled garden while the "serious research forum" is wide open!

[Kevin Buzzard]

The reason is that the serious research forum is being moderated by a serious dedicated team, and the informal play space doesn't have that luxury

[Mario Carneiro]

I don't know about that. As a moderator I could count the number of times I needed to take some kind of moderating action on one hand

[Mario Carneiro]

Zulip is amazingly well self-regulated

[Arthur Paulino]

Zulip is also a bit underground (I had never heard of Zulip before knowing about Lean), whereas Discord is a widely known place, with lots of bots wandering around

[Kevin Buzzard]

@crab if you want an invite then ping me, but I don't post them publically. Don't expect to see much computer science or Lean 4 chat though; it's just people doing mathlib and Lean 3, so it might not be your thing.

[Junyan Xu]

You need a separate account for each Zulip "server", and can't easily switch between servers within a page or in the app; for Discord (or Slack) this is just one click. I think it makes Zulip visitors more purposed and trollers/spammers less likely to show up.
(edit: Hmm, Zulip desktop app also supports multiple organizations (not called server here), but not the web version. But I imagine you'd be asked to re-login to an organization if you haven't visited it for a while. And indeed as Arthur Paulino said, Discord is much more popular; I count I've joined 64 Discord servers, but the number of Zulip servers I've ever seen is less than 10.)

[Arthur Paulino]

Kevin Buzzard said:

The reason is that the serious research forum is being moderated by a serious dedicated team, and the informal play space doesn't have that luxury

I think the key factor is not moderation, but maintenance. The Lean Zulip organization is maintained by the same folks who make Lean evolve and come true. And it's indeed a privilege.

[crab]

So what is the final conclusion? We just have a zulip chat? No extra discord server? I doubt people would join it either way if there is one.

[crab]

In truth, I think discord scores much hire for general chatting. Also, zulip channels are just discord channels with threads, so discord is actually a plus to zulip, IMO

[crab]

There could be help channels in the discord server for just threads, which would replicate zulip, and another for just text chatting, where you could make threads as well

[crab]

i think a discord server would be great

[crab]

I’m just thinking whether it is worth it to create one

[Arthur Paulino]

Discord doesn't allow fluent $\LaTeX$ like Zulip does. And in Zulip we can write code with syntax highlight of many languages, including our beloved Lean

lemma my_lemma {a : ℕ} : a = a := rfl

Here we can also customize links like #10000

[crab]

Someone can add discord highlighting

[crab]

also, the drawbacks you said are not that big of a deal, except for maybe the latex

[Arthur Paulino]

Custom links are important. #mwe is used several times, for example

[crab]

Then slack could be a possible option

[crab]

$\mathbb{R}$

[crab]

hmm, no latex

[Arthur Paulino]

Use double "$"

[Arthur Paulino]

$$\mathbb{R}$$ → $\mathbb{R}$

[crab]

Ah

[crab]

That’s neat

[crab]

There is a discord bot that can render latex

[Arthur Paulino]

That's over-engineering. Plus, this is not the main point. Discord was primarily designed for gaming. That's why they have a channel-based structure and even voice channels available

[crab]

Right, but i still think it would be useful

[crab]

Should I try to make a lean discord as an experiment?

[crab]

im certain that it will work

[Kyle Miller]

Arthur Paulino said:

Discord was primarily designed for gaming.

Zulip, on the other hand, was made by some MIT-folk who wanted to make a modernized Zephyr (roughly: a campus-wide IRC-like system; Zulip's streams/topics are something like Zephyr's classes/instances). Everyone who was serious about Zephyr would keep a screen session with a Zephyr client open since the protocol didn't offer any kind of message persistence. Zulip even has a Zephyr bridge, as an ultimate Zephyr client.

[Mario Carneiro]

I think that the main argument against is that it would split the community. Technical arguments are all well and good for whether to switch (and I don't think there is a compelling argument here, compared to the original gitter -> zulip move), but for creating a new venue, unless the target audience is significantly different, one or the other will dry up in short order, and/or the overall quality will diminish since people don't know where to hang out.

[crab]

Maybe the discord could be for just general chatting mainly

[crab]

i find that hard to do in zulip, because you need like a topic

[crab]

there could be a few help channels for people who only use discord

[Mario Carneiro]

that sounds like a plus in my book

[crab]

Why?

[crab]

i mean, the problem with general chatting is that the topic changes very fast

[Mario Carneiro]

I'm not sure why we need aimless chatting, there is a lot of material on zulip already and we don't need to lower the signal-to-noise ratio on top of it

[Mario Carneiro]

and zulip discussions can get plenty sidetracked

[crab]

What’s wrong with aimless chatting?

[crab]

like, I’ve had a general topic question about the lean logo in an image, and it went really quickly to lean’s implementation. A moderator had to split the thread, but no one really used the thread about the logo. It produces clutter

[Mario Carneiro]

I'm not sure what you mean, both topics got some coverage

[Mario Carneiro]

that sounds like everything worked as intended

[Huỳnh Trần Khanh]

I took the liberty of making a Discord server. our server will be informal and programming oriented. here's an invite: https://discord.gg/hAJ4dudARs

I'm not sure who will be our moderators, that will be determined via community consensus. democracy ftw! let's try this out and see if this works or not

[crab]

Eh

[crab]

Huỳnh Trần Khanh said:

I took the liberty of making a Discord server. our server will be informal and programming oriented. here's an invite: https://discord.gg/hAJ4dudARs

I'm not sure who will be our moderators, that will be determined via community consensus. democracy ftw! let's try this out and see if this works or not

Did you make it right now?

[Huỳnh Trần Khanh]

yes, you can join it now

[crab]

What are garden variety programmers?

[Huỳnh Trần Khanh]

ordinary programmers like me

[crab]

i suggest you name it Lean Community

[crab]

and put the lean logo for the server icon

[crab]

At least for the meantime

[Mario Carneiro]

hm, that seems a bit presumptuous if the leanprover-community maintainer team isn't involved

[crab]

really?

[crab]

then Lean could be fine

[crab]

Or Lean Programming Language

[Mario Carneiro]

that one is even worse, it suggests MS is involved

[crab]

woah what

[crab]

how

[Mario Carneiro]

It sounds official

[crab]

Why would you not want it to?

[Mario Carneiro]

you could put "unofficial" in the name, or try to make it more official

[Huỳnh Trần Khanh]

yeah I agree with Mario. I don't want people to think that our server is the Lean server

[Huỳnh Trần Khanh]

(deleted)

[crab]

what is the lean server? This?

[Mario Carneiro]

This zulip instance is pretty official, yes

[crab]

Ah ok

[crab]

then Unofficial Lean Discord could be fine

[crab]

or just Lean Discord

[Huỳnh Trần Khanh]

no objections right? can I go ahead and rename our server to Unofficial Lean Discord?

[crab]

Don’t you think Lean Discord sounds better?

[crab]

Ah, and putting at least some Lean logo would do good for the server icon

[Mario Carneiro]

looks like Kyle's "the scream" lean logo is already there

[crab]

”the scream”?

[crab]

How is it a lean logo?

[crab]

lol

[Huỳnh Trần Khanh]

lol changed to the official one

[crab]

Cool. Could you make me mod? I have some ideas

[crab]

and To add all the channels

[Huỳnh Trần Khanh]

you have mod rights now

[crab]

Thanks

[Eric Wieser]

Regarding a remark above, some of us have already been in touch with discord about adding lean syntax highlighting, and the answer was basically "no, because we just use X library", and X library says "new languages are no longer accepted, distribute them yourself as plugins"

[Eric Wieser]

Sure, you could write a discord bot to render lean code to an image, but... That would be awful?

[Bhavik Mehta]

Yeah this was briefly discussed in the early stages of the xena server, it's particularly annoying because you wouldn't be able to copy-paste the code either

[Eric Wieser]

Especially when compared to just using Zulip which doesn't need such hacks

[crab]

Someone can add lean syntax highlighting

[crab]

https://github.com/highlightjs/highlight.js/

[crab]

I mean, I understand your point

[Eric Wieser]

https://github.com/leanprover-community/highlightjs-lean already exists

[crab]

debut discord syntax highlighting doesn’t have to be the best

[Eric Wieser]

The Highlightjs repo ("X library" above) doesn't accept contributions of new languages any more

[Eric Wieser]

So no, it is not possible for anyone to do what you ask, without either paying highlightjs lots of money or paying discord even more money to change their minds

[Bhavik Mehta]

See also https://github.com/highlightjs/highlight.js/pull/1689 and https://github.com/highlightjs/highlight.js/pull/2464

[crab]

Hmm

[crab]

Where is it possible to advertise the discord server?

[crab]

@Kevin Buzzard said they would help with that

[Arthur Paulino]

I'd recommend setting some kind of goal for the server first, so people can have a motivation to join. Theorem proving is not nearly as popular as traditional programming

[crab]

Right

[crab]

what kind of goal do you mean? We just want to support the lean community

[Arthur Paulino]

For example, Kevin's server has a specific purpose of being a place where people talk about Lean 3/mathlib/mathematics in the context of the course he teaches

[Arthur Paulino]

Supporting the Lean community is too vague. It doesn't say anything about what actually happens in the server

[crab]

The discord has the purpose of chatting more comfortably

[crab]

about everything related to lean

[Huỳnh Trần Khanh]

I still want our server to be more programming oriented. combinatorics, data structures, program verification, etc. things that proper mathematicians hate to do

[crab]

also, https://discord.gg/nDX85DPF

[crab]

just repasteung the link

[crab]

Huỳnh Trần Khanh said:

I still want our server to be more programming oriented. combinatorics, data structures, program verification, etc. things that proper mathematicians hate to do

Good ideas

[crab]

https://github.com/leanprover-community/leanprover-community.github.io/tree/newsite/data We could add a discord.md to this

[crab]

pr

[crab]

https://github.com/leanprover/leanprover.github.io/pull/84

[Arthur Paulino]

I'm afraid it's a bit too early to consider referencing the server in the official community website. There hasn't been any substantial benefits from it yet

[crab]

Im aware, but, it the future it may be a consideration

[crab]

i honestly agree with you tbh

[Kevin Buzzard]

crab said:

also, https://discord.gg/nDX85DPF

I can tweet about it if you like. Let me know when you think it's ready to advertise

[crab]

We should get a few more people

[Mario Carneiro]

Huỳnh Trần Khanh said:

I still want our server to be more programming oriented. combinatorics, data structures, program verification, etc. things that proper mathematicians hate to do

I want to note that we have the #metaprogramming / tactics, #Program verification and #Type theory streams for more programming oriented discussion, and if that's not specific enough you can also create your own stream. There doesn't seem to be much traffic on these topics though

[Patrick Massot]

crab said:

i suggest you name it Lean Community

Why not calling it "Lean for teenagers"? That would make the intend clear and it wouldn't sound too official.

[Patrick Massot]

I think it's a really good idea that you get a place to discuss Lean where you feel more comfortable than here.

[crab]

But that we feel seclusive of older people who would like to join

[Marc Huisinga]

crab said:

There could be help channels in the discord server for just threads, which would replicate zulip, and another for just text chatting, where you could make threads as well

I don't think Discord works for a community the size of Lean's at all. I've yet to see a single large public Discord community with many active contributors that is anything but endless spam, noise and incomprehensibly interleaved arguments and topics of discussion. Discord threads also don't seem to work nearly as well as Zulip threads do, mostly because nobody is willing to use them. I'm convinced that this community simply wouldn't exist as it does now on any of the other platform.

FWIW, I feel like this Zulip already strikes a decent balance between casual and professional conversations about Lean, with the only downside being that you create new topics every once in a while when a conversation gets too off-topic. That probably disincentivizes posting your every thought, but as far as I'm concerned (I spend most of my time here reading, not posting), that's a benefit :grinning:

The only thing that's perhaps missing is some kind of strictly off-topic stream, and I'm not sure whether a chat or a topic format would be better suited for that, or whether it's desirable at all.

[Kevin Buzzard]

Call me old-fashioned but I really like the fact that there's no off-topic stream. I think it gives this place a more professional feeling. I also don't like it when people don't use their full real names. Sometimes I have decided not to respond to someone asking a question here because they are not using their full real name. However on the Xena discord I don't care about these things at all. I tell people that this place is a serious research forum, not a chat room

[crab]

I disagree, honestly, the big discord server with great communities

[Eric Wieser]

I think you missed a word in that sentence, and so can't work out what you meant

[crab]

crab said:

I disagree, honestly, the big discord server with great communities

I have seen big discord servers with great communities

[Marc Huisinga]

Kevin Buzzard said:

Call me old-fashioned but I really like the fact that there's no off-topic stream. I think it gives this place a more professional feeling.

That's one of my reservations as well.

crab said:

crab said:

I disagree, honestly, the big discord server with great communities

I have seen big discord servers with great communities

I'm not saying that large public Discord communities cannot be good or helpful, but that there tends to be lots of noise and interleaved discussion in single channels, which makes it very hard to follow if you are not constantly paying attention to what topics are being discussed right now. I can also believe that heavily moderated Discords solve this issue by setting up many channels that effectively take on the role of topics in Zulip and funneling discussion there, but that seems like a lot of manual effort for something that Zulip more or less does by itself already.

[Eric Wieser]

crab said:

I have seen big discord servers with great communities

Greatness can be measured on multiple axes. I'm sure big discord servers can be fun and engaging, but I suspect it is hard for them to assist with productivity to the same extent this Zulip does (simply due to the worse and underused threading model).

[Arthur Paulino]

As far as I can tell, Zulip also accomplishes the goal of being an organized repository of knowledge, definitely like a better designed forum. This is not (and has never been) the goal of Discord. As I said before, Discord was designed to suffice the needs of gamers, who need to interact as instantaneously as possible. Even Discord threads are meant to die out after a few days (they literally have a validity deadline). Whatever was said 1~2 weeks ago in Discord doesn't matter anymore.

In contrary, the interaction speed needed for discussions involving Lean is way slower. We need the time to think deeply about our questions and especially about the answers we get. And every discussion matters and is already placed/archived properly because of Zulip's thread-based structure.

The most professional thing I was able to accomplish with Discord was paired coding/debugging sessions, in which one person shares their screen in a voice channel and the group discusses the code. And this doesn't seem to be the style of Lean contributors. At least not for now :+1:

[Kevin Buzzard]

If there was one thing from the Xena discord I wish we had here it would be the "let's just hop onto a voice channel and you share your screen and I fix up your messed up project" option which we have there. However of course you can just do this here, just via some other server like big blue button or whatever

[Kevin Buzzard]

But in some sense this is just for helping out new members. Once people have got going and have learnt how to ask good questions ie post MWEs, you don't even need the voice channel

[Johan Commelin]

If you write a message on Zulip, there are these buttons like "Upload files" and "Preview" below the input box. There's also "Add video call". Did anyone ever try that? I just always reach for Zoom. But maybe the feature is just there, staring in our faces.

[Arthur Paulino]

Going beyond the beginner's realm, pair programming to tackle some nasty/complex problem is a rather common practice in CS

[Joscha Mennicken]

It just generates a link to a jitsi meeting, nothing more: Click to join video call (demo link)

[Matthew Ballard]

You can also switch from Jitsi to Zoom