Suppose you take a piece of GPL code and write an English document sketching a proof of correctness of the code. Would your document be considered a derivative of the code. Can it only be distributed under GPL?
Are you including the code itself in your "proof" document, or only referring to it (e.g. as a reference, hyperlink, or something like that)?– BrandinJul 16, 2020 at 12:41
Not including code. Just refering to it as hyperlink.– Abhishek AnandJul 16, 2020 at 13:50
2Is the proof proving the algorithm, or that the code implements the algorithm correctly? My gut intuition says the first would not be a derivative work, but the second, I really don't know about. You might like to ask at the Law site, or get a lawyer, if the answer is really important to you.– curiousdanniiJul 16, 2020 at 14:03
This is an interesting question, because you are mixing code copyright and copyright of articles and facts, which work quite different.
The easiest parts are the facts. A mathematical proof is something that deserves academic acknowledgement, but no copyright, as it just states facts and facts cannot be copyrighted.
Describing the proof may warrant copyright. The full article certainly is copyrighted. The proof in formal math language may be not as it is merely stating the facts. But what about proofs written in prose?
The final part is the code. When you do a rigorous proof, you probably include the code or include facts about the code in a way that it can be written again using your article. And the code by itself is copyrighted by whoever wrote it.
Note that there may be copyright clauses for academic works, that may permit including GPLed code regardless of the copyright of the article.
For a definite answer I second @curiousdannii that law.stackexchange.com may be the more appropriate site for the full details.