[flagged]

Producing a formalized proof from a non-formalized proof in a paper or book should not be considered a violation of copyright.

	▲	pfdietz 3 hours ago \| parent [-]
		Indeed; one cannot copyright mathematical ideas, only their specific expressions. And the formalization is a different expression.