Teaching Interactive Proofs to Mathematicians

Mauricio Ayala-Rincón
(Universidade de Brasília)
Thaynara Arielly de Lima
(Universidade Federal de Goiás)

This work discusses an approach to teach to mathematicians the importance and effectiveness of the application of Interactive Theorem Proving tools in their specific fields of interest. The approach aims to motivate the use of such tools through short courses. In particular, it is discussed how, using as case-of-study algebraic notions and properties, the use of the proof assistant Prototype Verification System PVS is promoted to interest mathematicians in the development of their mechanized proofs.

In Pedro Quaresma, Walther Neuper and João Marcos: Proceedings 9th International Workshop on Theorem Proving Components for Educational Software (ThEdu'20), Paris, France, 29th June 2020, Electronic Proceedings in Theoretical Computer Science 328, pp. 1–17.
Published: 30th October 2020.

ArXived at: http://dx.doi.org/10.4204/EPTCS.328.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org