Towards Automatic Transformations of Coq Proof Scripts

Nicolas Magaud

Proof assistants like Coq are increasingly popular to help mathematicians carry out proofs of the results they conjecture. However, formal proofs remain highly technical and are es…