Can part of mathlib be public domain?

Stream: general

[Mark Andrew Gerads]

I made a new file that I am contributing to mathlib: https://github.com/leanprover-community/mathlib/pull/18116
Because all the other files I looked at were Apache 2.0, I was planning on following suit, as I assumed all of mathlib needed to be licensed with Apache 2.0, but I would prefer my file be in the public domain if possible. Is this allowed?

[Kyle Miller]

I'm not sure this question has come up before. I think our collective understanding is that mathlib is copyrighted by its respective authors, but by submitting contributions to the mathlib project, each author agrees to license their contributions under the Apache 2.0 license.

A license is a way to allow other people to use your work without violating your copyright. You can license your own work under any number of licenses to any number of people.

My own understanding is that in a number of places in the world, it's not possible to put your own work into the public domain, and the original author retains some sort of copyright in perpetuity (ex: moral rights in France). If your own jurisdiction allows it, you can put your work into the public domain. I don't think we need to record this fact in mathlib's source code -- you can go and post the code somewhere else with the appropriate notice that it's been released to the public domain.

[Kyle Miller]

(And of course, a disclaimer that I'm not a lawyer, etc. etc. I've just read about this before to try to figure out who "owns" mathlib or other open source projects.)

[Mark Andrew Gerads]

Okay, I will keep a copy posted in my own repository, and have it under the public domain there. Having 2 licenses makes sense for this, I guess. Thanks for answering.

[Eric Wieser]

Of course, you could argue that any review suggestions you received were Apache-licensed and therefore not yours to release into the public domain without agreements from their authors

[Kyle Miller]

You might consider public-domain equivalent licenses if you want to be careful, like CC0. This one attempts to transfer your copyright to the public domain, but wherever that's impossible it tries to grant licenseholders arbitrarily broad rights to use your work as a fallback.

[Kyle Miller]

(That's not a response to Eric, by the way, we just sent messages at the same time.)

[Eric Wieser]

Also note that that anyone who disagrees with the Apache license will not be able to do much with your public domain code while the files it imports from mathlib are not public domain!

[Mark Andrew Gerads]

Eric Wieser said:

Of course, you could argue that any review suggestions you received were Apache-licensed and therefore not yours to release into the public domain without agreements from their authors

I guess I will be content with having my first draft in the public domain then.

[Patrick Johnson]

There are examples where one of the contributors to an open-source project insists to use a different license than the rest of the project. Maintainers usually accept that. For instance, my friend Thomas Andreyevich once contributed to a large open-source MIT-licensed repository, but insisted to have his work published under the Unlicense (public domain). The maintainers were happy with that.

[Eric Wieser]

That seems a bit weird, because doesn't the unlicense allow me to take the work, remove the unlicense text, and republish it as MIT?

[Kevin Buzzard]

Eric Wieser said:

Also note that that anyone who disagrees with the Apache license will not be able to do much with your public domain code while the files it imports from mathlib are not public domain!

This is not the first time I've seen this apparently contradictory situation: IIRC @William Stein 's modular forms code in magma was all public domain but relied on closed source material to function.

[Patrick Johnson]

Eric Wieser said:

That seems a bit weird, because doesn't the unlicense allow me to take the work, remove the unlicense text, and republish it as MIT?

What is the meaning of "allow" there? If you mean legally, I have no idea, because to me copyright is nonsense and I live in a country which doesn't recognize any copyright laws, so I can't answer that. The point of having the Unlicense is to say "I don't care about copyright". So, whoever wants to respect the author (by saying "he wrote this piece of code"), they should also respect the author's decision by saying "and he doesn't care about copyright" by allowing the piece of code to be in the public domain.

BTW, here is the example: https://github.com/Automattic/node-canvas/pull/1295/files

[Eric Wieser]

So, whoever wants to respect the author (by saying "he wrote this piece of code"), they should also respect the author's decision by saying "and he doesn't care about copyright" by allowing the piece of code to be in the public domain.

The code is in the public domain whether or not the announcement of such resides in HEAD of the repo though, I assume; and the Unlicense is rejected by the legal departments of some corporations, which might provide motivation to the maintainers to relicense it after the fact

[François G. Dorais]

As far as I can tell, there is no conflict between making your work public domain and also releasing it under the Apache License. The copyright owner is allowed to release their work under any conditions they choose to anyone they want. Once you release your work to someone you are bound by the agreed conditions, which may prevent or restrict you from further releasing the work. Since the Apache License is non-exclusive, there is no apparent breach the Apache License by also declaring your work to be in the public domain.

The easiest way to declare your file to be in the public domain is to change the first line of the notice from "All rights reserved" to "No rights reserved". Public domain is a declaration that you waive all rights associated to authorship of the work. There's no form for that, you just have to make your intent clear. It's a lot like putting a "FREE" sign on something you own, that doesn't change your ownership by itself but it does make it clear that anyone can take that think and make it their own without fear of being accused of theft.

[Yury G. Kudryashov]

Note that "public domain" has no meaning in the copyright law in most countries. People use licenses like CC-0 or WTFP to make it "public domain" worldwide.