Discussion on Community Policies

Stream: general

[Matthew Ballard]

Discussion space for #announce > Community Policies

[Robin Carlier]

After what happened in #Machine Learning for Theorem Proving > Lean Zulip Chat Dataset, can I ask that the moderator team or owners of this instance (the FRO? The "leanprover organization"? Mathlib maintainers?) also release a clear statement the current policies on scraping the messages in this chat for AI training and the current license status of the code snippets posted here?

[Kevin Buzzard]

Clarification on the ownership issue: I think that in practice the owners/admin/maintainers of this Zulip instance are essentially exactly the mathlib maintainers + Leo + Sebastian (the cofounders of the FRO).

[I say "essentially exactly" because this is a manual process, and every now and then a new maintainer says "oh I'm not a Zulip maintainer yet", or we notice that a former Mathlib maintainer is still a Zulip maintainer etc]

[Chris Bailey]

Robin Carlier said:

the current license status of the code snippets posted here?

That's up to whoever wrote the snippet, not the org owners.

[Robin Carlier]

Right, I finally found the sections of the zulip TOS that states this. TLDR; you own your snippets (phew).
@Kevin Buzzard, among those in the list you gave, which ones are the ones paying for the infrastructure needed to run this server (i.e the actual "Zulip customer" by their TOS)? Am I right to assume that’s the FRO?
(Sorry if this is too out-of topic for this thread, I don’t intend to derail the discussion too much. Feel free to move this away).

[Sebastian Ullrich]

We're using the free plan

[Robin Carlier]

Oh, wow. I was not expecting a server with this size and this traffic could run off a free plan.

[Kevin Buzzard]

We give them free advertising in return.

[Yaël Dillies]

Are we really using the free plan? It's free for us, but I thought it was because we are a sponsored community.

[Sebastian Ullrich]

Alright, I guess it's called the Free Standard plan specifically

[Jireh Loreaux]

But we're not paying for it. Zulip sponsors us, right?

[Sebastian Ullrich]

Yes, that makes it free