Comment by penteract

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