Teaching Interactive Proofs to Mathematicians
Mauricio Ayala-Rinc\'on (Universidade de Bras\'ilia), Thaynara Arielly, de Lima (Universidade Federal de Goi\'as)
TL;DR
This paper explores an educational approach to motivate mathematicians to adopt Interactive Theorem Proving tools, specifically using PVS, through short courses focused on algebraic concepts.
Contribution
It introduces a teaching method that demonstrates the practical benefits of proof assistants to mathematicians, fostering their engagement with mechanized proofs.
Findings
Mathematicians showed increased interest in using PVS after the courses
The approach effectively demonstrated the relevance of interactive proofs in algebra
Short courses can motivate adoption of proof assistants in mathematical research
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.