Copyright when formalizing a book

Stream: general

[Mario Xerxes Castelán Castro 🇲🇽]

If I make a formalization in Lean of all the theorems and my own solutions to exercises in a mathematics book, would that be a break of Copyright?

[Kim Morrison]

Generally speaking, yes, translating a work (whether between human languages, or a between computer languages, and hence presumably by extension translating from a human language to a computer language!) counts as a derivative work, and hence is in principle covered by copyright law. What there is in terms of precedent of enforcement here, I don't know.

[Snir Broshi]

Why is it not free-use, assuming USA?

[Yan Yablonovskiy 🇺🇦]

Snir Broshi said:

Why is it not free-use, assuming USA?

I feel that usually theorems come from literature and are helpfully collated into books at different stages of the subjects maturity. So I don't know if formalising theorems from a book, which would have its own references, is particularly problematic -- especially if referenced.

But you can imagine a situation where you can transcribe a book in too much detail including its exact exposition and structure in your Lean blueprint, which might make copyright more applicable.

[David Michael Roberts]

Facts in an of themselves are (as far as I understand) not copyrightable. Expression of facts is, in contrast. Anyone can write their own history book listing a bunch of events using the names etc as appropriate, even when this is already in a copyrighted work. But the manner of expression of the historical events in the existing work is not something you can copy.
Mathematical expressions I believe falls under the same kind of thinking. One can creatively express a formula, say as an artwork presenting the equation as a giant graffiti tag, and this expression has copyrightable content. Assembling formal proofs of a list of theorems feels to me like assembling your own history book, but IANAL.
Also, while one might argue that the flow of the sequence of definitions and theorems etc is a specific expression, the formalisation is almost surely not going to be an identical sequence of definitions and theorems, and moreover the manner of expression is a very large transformation, not merely something like translating text from one human language to another. Much is added!

[Mario Xerxes Castelán Castro 🇲🇽]

David Michael Roberts ha dicho:

Also, while one might argue that the flow of the sequence of definitions and theorems etc is a specific expression, the formalisation is almost surely not going to be an identical sequence of definitions and theorems, and moreover the manner of expression is a very large transformation, not merely something like translating text from one human language to another. Much is added!

The point of this particular formalization would be to stay as close to the source book as practical.

[Thomas Murrills]

I would hope that in the U.S. even going theorem-by-theorem would be fair use by virtue of being transformative, and being for “nonprofit educational purposes” would also count towards fair use…but I also am not a lawyer. :)

(Note: if you leave out the prose, I feel it becomes very hard to argue that the formalization “supersedes the purpose of the original”. If you do copy the prose, it sounds like a much trickier case…)

[Violeta Hernández]

I'd just like to make the general remark that copyright as it exists in the books is a completely different entity to copyright as is enforced on a daily basis.

[Violeta Hernández]

I'm not a lawyer, but I wouldn't worry too much about something like this unless you're going out of your way to call attention to it and monetize it.

[François G. Dorais]

Why not contact the author (or other copyright owners)? I think many authors will be supportive and willing to discuss legal issues with you in a constructive manner.

[François G. Dorais]

For example, I've never heard of an author/publisher of a math book rejecting that their work be translated in another language.

[Snir Broshi]

François G. Dorais said:

Why not contact the author (or other copyright owners)?

IMO this is a major barrier to entry for a hobby project, I would never do such a thing (unless I have to). If they agree it puts a lot of pressure on completing the project and not abandoning it, which is not fit for hobby projects.

[David Michael Roberts]

If one thinks that a maths book is merely the definition and theorem statements, and proofs, then this is a very impoverished view. One would hope the book has plenty of expository prose, especially if it's a textbook, which from the mention of exercises, it might be.

[François G. Dorais]

Snir Broshi said:

François G. Dorais said:

Why not contact the author (or other copyright owners)?

IMO this is a major barrier to entry for a hobby project, I would never do such a thing (unless I have to). If they agree it puts a lot of pressure on completing the project and not abandoning it, which is not fit for hobby projects.

I infer that you haven't met any textbook authors, your portrayal of them as antagonists is very unusual.

[Snir Broshi]

François G. Dorais said:

I infer that you haven't met any textbook authors, your portrayal of them as antagonists is very unusual.

I don't see where you got that portrayal from, what about my statement says/implies something about the character of textbook authors?

[Snir Broshi]

FWIW I did meet a few textbook authors (as professors teaching a class), and they were cool

[Yan Yablonovskiy 🇺🇦]

Snir Broshi said:

François G. Dorais said:

I infer that you haven't met any textbook authors, your portrayal of them as antagonists is very unusual.

I don't see where you got that portrayal from, what about my statement says/implies something about the character of textbook authors?

I think it might just be saying that textbook authors will probably mostly be fine with it if you ask them(i.e it isnt as huge of a barrier as it might seem).

[Snir Broshi]

Yan Yablonovskiy 🇺🇦 said:

Snir Broshi said:

I don't see where you got that portrayal from, what about my statement says/implies something about the character of textbook authors?

I think it might just be saying that textbook authors will probably mostly be fine with it if you ask them(i.e it isnt as huge of a barrier as it might seem).

But I never said that was the barrier. The contacting itself is the barrier, not the possibility of a negative answer.

[Timothy Chow]

I feel that this is one of those cases where, perhaps because our society is so litigious, a question is being framed as a legal question when it is better to form it a question of etiquette. The legal question should only need to be raised if the situation has gone sour for some reason.

As others have said, it's highly unlikely that a court would determine that a Lean formalization infringes copyright; in the worst case, you could make an excellent argument that the formalization is transformative. But why start with the worst-case scenario? If you're going to create a formalization and make it public, then it's simply polite to inform the authors. If you're worried about the pressure to follow through on your implied promise, then just wait until the project is completely finished before asking the authors if they're okay with your making your formalization public.

[David Kinkead]

That approach sounds right to me. I'm currently working on exactly this sort of formalisation of Lawvere and Schanuel's Conceptual Mathematics and would certainly have contacted the authors before making it public if either were still with us. My sense is that as long as the formalisation remains non-commercial in nature, limits its use of extracts from the original work, and is careful when citing those extracts, then the question here is almost certainly one of etiquette rather than law. (In the hilariously unlikely event that I get hit with a takedown notice, I'll certainly report back!)

[Mario Xerxes Castelán Castro 🇲🇽]

François G. Dorais ha dicho:

Why not contact the author (or other copyright owners)? I think many authors will be supportive and willing to discuss legal issues with you in a constructive manner.

The author is dead. It is Michael Spivak.

[Mario Xerxes Castelán Castro 🇲🇽]

I agree with the viewpoint that it is unlikely to be a problem if the formalization is not commercialized.

[François G. Dorais]

Michael Spivak's publishing company still exists: https://mathpop.com/