论文标题
向数学家教授互动证明
Teaching Interactive Proofs to Mathematicians
论文作者
论文摘要
这项工作讨论了一种向数学家讲授交互式定理在其特定感兴趣领域中证明工具应用的重要性和有效性的方法。该方法旨在通过短期课程来激励使用此类工具。特别是，讨论了如何使用所在案例代数概念和属性，在开发其机械化证明时，使用证明助手原型验证系统PV被提升为利益数学家。
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.
