Mathlib and copyright ownership

Stream: general

[Karl Palmskog]

Given the following tweet, I would be interested in how copyright is handled for Mathlib: https://twitter.com/XenaProject/status/1276985859552825346

What happens usually in open source is that copyright is retained by each author, so the definition in Lean of perfectoid spaces is owned by its authors. For something like Lean code to "never be owned by anyone", the only way I know would be to set up an organization to which all copyright is assigned, like the FSF does with GNU project contributions. Is this what is done currently?

Perfectoid spaces! https://link.springer.com/article/10.1007/s10240-012-0042-x . Yours for only £29.95 from Springer Verlag. Perfectoid spaces! https://github.com/leanprover-community/lean-perfectoid-spaces/blob/43954f64ce4afdf4fa39e2aeef8ec43826b24f2a/src/perfectoid_space.lean#L54 . A well-defined term in a well-defined type theory. Hosted by @github , with an Apache 2.0 license. Free software. Can never be owned by anyone.

- The Xena Project (@XenaProject)

[Johan Commelin]

I am far from an expert, but I think Kevin meant that this code can not be put behind a paywall.

[Jalex Stark]

"own" is a weird word

[Johan Commelin]

Personally, I don't care about copyrights... people can do whatever they want with the code I write.

[Simon Hudon]

I believe the authors still retain the ownership in the case of mathlib

[Johan Commelin]

If they want to claim that they wrote the code... I don't care.

[Jalex Stark]

does ownership mean that they can later unpublish it?

[Johan Commelin]

But you are asking about mathlib, not about my opinion. Currently I think all mathlib files (with nontrivial content) have a copyright header that mentions the Apache License.

[Karl Palmskog]

Johan Commelin said:

I am far from an expert, but I think Kevin meant that this code can not be put behind a paywall.

The Apache-2.0 license absolutely permits putting copies of code behind a paywall. But I guess you mean something like: "the Lean community will endeavor to always provide this code for download for free"

[Karl Palmskog]

Jalex Stark said:

does ownership mean that they can later unpublish it?

Most license dedications can't be revoked. However, they could also license it under other licenses, such as proprietary ones.

[Johan Commelin]

Well, our repo is not behind a paywall, and organisations cannot force us to take it down. So the perfectoid repo should in principal always stay around. Free to read for everyone with an internet connection.

[Jalex Stark]

so i guess there's a question of whether we can make the legal reality match up better with our interpretation

[Simon Hudon]

The other variable @Johan Commelin is for us to not lose interest and abandon the website or delete the account

[Jalex Stark]

and karl is suggesting this social technology of forming an org with a mandate to keep providing this code for free

[Johan Commelin]

Yup, agreed. Hence the "in principal" (@Simon Hudon)

[Karl Palmskog]

Johan Commelin said:

Well, our repo is not behind a paywall, and organisations cannot force us to take it down. So the perfectoid repo should in principal always stay around. Free to read for everyone with an internet connection.

We have discussed this issue in coq-community. GitHub can absolutely shut repos/websites down (whether by policy or accident). Hence, many of our project repos are mirrored on multiple open platforms.

[Simon Hudon]

That's a good idea

[Johan Commelin]

We have local clones, so we can host it in another place as soon as github acts up

[Simon Hudon]

Where do you mirror them?

[Johan Commelin]

I guess gitlab and sourcehut are obvious candidates?

[Karl Palmskog]

GitLab for one

[Simon Hudon]

Is there a mechanism to push everything from the github repos to gitlab or others on a regular basis?

[Jalex Stark]

could it be implemented as a GitHub Action?

[Bhavik Mehta]

GitLab lets you continuously mirror from github automatically, I think

[Jalex Stark]

this mirroring can be done unilaterally, then

[Karl Palmskog]

Here's our discussion on backup etc. so far: https://github.com/coq-community/manifesto/issues/76 --- We have also considered platforms like Zenodo: https://github.com/coq-community/manifesto/issues/75

In any case, for the "free availability" goal to hold, I think these issues have to be considered.

[Johan Commelin]

The bigger problem is all the "extras" that github offers: issues and PRs. If those get taken down, it's harder to recover the info, because it's not stored in the repo.

[Karl Palmskog]

Johan Commelin said:

The bigger problem is all the "extras" that github offers: issues and PRs. If those get taken down, it's harder to recover the info, because it's not stored in the repo.

they can be exported (regularly) via GitHub's API

[Johan Commelin]

But is gitlab compatible with it?

[Johan Commelin]

Maybe we only want to backup the stuff, and not mirror things like issues. I guess that would quickly become confusing anyway.

[Karl Palmskog]

if you have the JSON or whatever, you could always convert it (we did this for imported Bitbucket repos)

[Karl Palmskog]

Jalex Stark said:

and karl is suggesting this social technology of forming an org with a mandate to keep providing this code for free

I wasn't suggesting to go the FSF route and force reassignment of copyright for contributions, I'm just saying this is what one has to do to if the goal is to make sure nobody owns the code. In coq-community at least, we don't mind if everybody owns their code themselves, even though it becomes very problematic if one wants to change license (e.g., from GPL2 -> Apache-2.0)

[Jalex Stark]

i think it's not a crazy goal; I would guess it is not worth the effort right now, but would not be surprised if it were worthwhile two years from now.

[Simon Hudon]

What would we gain?

[Karl Palmskog]

I think FSF does it mostly so they can take legal action against violators of the GPL. But Apache-2.0 is such a permissive license that it's hard to violate...

[Mario Carneiro]

I would like to move everything to public domain, but I think that's probably not possible because we have too much MSR code in mathlib

[Karl Palmskog]

public domain doesn't work in all jurisdictions, the closest we have used in coq-community is the Unlicense: https://unlicense.org (which has an MIT-like fallback)

[Jalex Stark]

If you increase the long-term availability of the code, you gain some probability mass on "the work we're doing on mathlib now is appreciated by people 40 years from now." But right now if you want to buy probability on that event, the most efficient thing to do is increase the number of good researchers contributing to mathlib.
("is my work still recognized 40 years from now" is a thing career mathematicians optimize somewhat hard for, I think)

[Mario Carneiro]

I mean by PD multilicensed PD / CC0 / unlicense / WTFPL of course :)

[Karl Palmskog]

well, that kind of PD at least renders the "ownership" issue moot (anyone can claim they own Mathlib)

[Mario Carneiro]

that works for me

[Mario Carneiro]

we even tried to sidestep that question pretty hard in the mathlib paper

[Mario Carneiro]

I think there are more than enough social institutions for apportioning credit in OSS projects without any need for copyright claims

[Simon Hudon]

Jalex Stark said:

If you increase the long-term availability of the code, you gain some probability mass on "the work we're doing on mathlib now is appreciated by people 40 years from now." But right now if you want to buy probability on that event, the most efficient thing to do is increase the number of good researchers contributing to mathlib.
("is my work still recognized 40 years from now" is a thing career mathematicians optimize somewhat hard for, I think)

I don't think that's a major stumbling block. Yes, mathlib is a mathematical artifact but it's also a software artifact. It's hard to find a piece of code that remains relevant for 40 years. The theorems proved today will still be true in 40 years but it is encoded in Lean. Will Lean still be around in 40 years? Maybe the language will be completely different maybe there will be something better

[Mario Carneiro]

I think this is a serious concern though, that is not really being currently addressed and will become a bigger problem as mathlib grows

[Mario Carneiro]

Lean is absolutely not "40-year proof"

[Mario Carneiro]

that doesn't mean it's impossible to have something that is

[Jalex Stark]

we'll learn a lot from porting mathlib to lean 4

[Mario Carneiro]

lean is notoriously volatile even among contemporary proof assistants

[Karl Palmskog]

I have worked on updating 20+ year old Coq code quite a lot, it's hard but usually works out in the end (due to Coq maintainers' compatibility policies)

[Johan Commelin]

One thing that I want, is that I can edit mathlib files without having the original author having legal rights about what the file should look like. But I guess that is not a problem with our current setup.

[Karl Palmskog]

the main value from 20+ year old code are definitions and theorem statements... if a development has been partitioned properly so that there aren't gigantic proof scripts for a single lemma, it usually works out. Paulson makes similar points about Isabelle here (when talking about porting from HOL Light)

[Jalex Stark]

i imagine that when lean stops being the best choice for developing math libraries, a fork of mathlib will be translated into a better language

[Mario Carneiro]

Metamath was definitely built to be "archival quality"; the spec has remained essentially unchanged from the 1991 version although it has grown in several backwards compatible ways

[Mario Carneiro]

The idea that your proofs will outlive you is part of the ethos

[Jalex Stark]

maybe all we need for lean proofs to survive is to be able to compile them down to metamath

[Simon Hudon]

I don't suppose we can expect the proofs to outlive the community.

[Mario Carneiro]

why not?

[Jalex Stark]

say everything in mathlib was compiled to metamath, and then everyone forgot about the existence of lean

[Mario Carneiro]

metamath proofs may not live on as metamath proofs necessarily, but the idea is that they will be forward ported in perpetuity

[Simon Hudon]

Especially with Lean, we've kept the code alive but adapting it through the myriad of breaking changes

[Jalex Stark]

then in the development of the next general mathematics library, you make heavy use of a mm_library_search

[Jalex Stark]

this is like relying on details checked by elders in ordinary maths

[Mario Carneiro]

@Simon Hudon The problem with this method is that it is very labour intensive and as soon as people decide that porting is no longer worth the effort, it dies

[Mario Carneiro]

having a stable "fallback" language is good for offloading developments where you don't care to upkeep them at that level

[Simon Hudon]

That's true but not many software project survive the lack of maintainers. We might want to get to a point where the breaking changes are less common or we track master less closely but it will have to keep being maintained

[Mario Carneiro]

I think you are highlighting the importance of a Project Gutenberg for formal proof

[Jalex Stark]

is a "Project Gutenberg for formal proof" an archivist who keeps the code runnable without developing it?

[Mario Carneiro]

right

[Jalex Stark]

do you prefer keeping code runnable to translating the code-base into metamath and then letting it bitrot?

[Mario Carneiro]

I imagine that the latter is less labor intensive because keeping a complicated program running on newer hardware can be challenging

[Jalex Stark]

for some appropriate definition of metamath C, is "reimplement the prover in metamath C" enough to translate all of the proofs to metamath?

[Mario Carneiro]

The main claim for reliability of metamath on future hardware is that it is really simple to write from scratch and this has been done over 20 times in almost every major language

[Mario Carneiro]

Metamath C is a bit of vaporware of my own devising, not to be confused with metamath :)

[Jalex Stark]

yes, I did mean to ask about the vaporware. the question is "do you think it's possible to write a language with the specified property?"

[Mario Carneiro]

yes, the goal was to outline what I think I can feasibly get done in ~1 year when my dissertation comes due

[Mario Carneiro]

(but that's a bit off topic for this thread, feel free to continue at #Program verification)