license: is a correctness proof of a piece of code a derivative of the code

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.