论文标题
证明：组织和验证一般数学知识的证明助手
Prove-It: A Proof Assistant for Organizing and Verifying General Mathematical Knowledge
论文作者
论文摘要
我们介绍了Prove-it，这是一家总部位于Python的通用交互式定理助理助手，其目的是使正式定理证明与非正式定理证明（通过中等培训）一样容易自然。证明 - 它使用了一个高度柔滑的jupyter笔记本电脑界面，该用户界面使用乳胶记录了交互和证明步骤。我们审查证明这对表达，判断，定理和证明的高度表达性表示；通过构建传统的证明，证明系统$ \ sqrt {2} \ notin \ mathbb {q} $;并讨论该系统如何避免Russell和Curry的悖论等矛盾之处。有关系统核心元素的附录中提供了广泛的文档。当前的开发和未来的工作包括对量子电路操作和量子算法验证的有希望的应用。
We introduce Prove-It, a Python-based general-purpose interactive theorem-proving assistant designed with the goal of making formal theorem proving as easy and natural as informal theorem proving (with moderate training). Prove-It uses a highly-flexible Jupyter notebook-based user interface that documents interactions and proof steps using LaTeX. We review Prove-It's highly expressive representation of expressions, judgments, theorems, and proofs; demonstrate the system by constructing a traditional proof-by-contradiction that $\sqrt{2}\notin\mathbb{Q}$; and discuss how the system avoids inconsistencies such as Russell's and Curry's paradoxes. Extensive documentation is provided in the appendices about core elements of the system. Current development and future work includes promising applications to quantum circuit manipulation and quantum algorithm verification.
