Mapping and Re-applying Mathematical Knowledge in Mechanical Theorem Proving

创造力被广泛认为是数学中的一项基本技能。这个过程很难具体说明，但我们知道，在人类身上，经验和冒险让我们能够开发出新的策略和概念模型。网络理论以及能够表示复杂数据结构的更先进的神经网络拓扑结构的发展，为自下而上地对数学概念之间的关系进行建模和分析提供了机会。生成性对抗网络建立在这个基础上，允许我们开发创造性的软件来处理和重新表达这些知识，并在交互和自动化定理证明中有许多应用，其中识别和重新应用新问题或情况的知识对于证明过程的所有阶段都是必要的。1994年，QED宣言提出了一个数学愿景，其中所有的证明在包括到一个整体的数字档案中时都被自动形式化。其动机包括：确保正确性，解决组织问题，改善传播和教育，以及启用元分析。二十多年后，这一愿景并未实现，但它仍然是相关的和可以实现的。QED档案的基础是并行构建一个类似QED的系统，一个交互定理证明器(ITP)，它可以通过自动化很大一部分过程来减少创建正式证明所需的劳动力和技术专业知识，促进更广泛的数学界采用它。因为与传统的数学过程相比，当代的信息技术转让计划的使用仍然困难和耗时。此外，大多数ITP使用不同的建构主义逻辑，这些逻辑比经典数学更具限制性，既限制了QED档案可以包含的内容，也限制了其条目的应用范围。该项目的预期实际贡献将是通过改进人类专家和自动定理证明者(ATP)如何利用先前的工作来提高ITP中的证明率。生成相关引理和策略的能力可以显著提高ATP的成功率。具体地说，使用基于网络的方法来执行这项任务有可能利用以前未开发的功能，这些功能在与传统技术作为整体的一部分结合时可以提高性能。这种映射也有潜力促进逻辑、软件和档案之间的互操作性或形式证明的自动翻译机制，以解决ITP的可用性问题。最后，在不改变自动建议技术操作语料库的情况下，任何自动建议技术的用处都是有硬限制的，找到组织这些库的最佳方式对于自动建议技术的持续改进是必要的。

Creativity is widely recognised as a fundamental skill within Mathematics. The process is difficult to specify, but we know that in humans, experience and risk-taking allow us to develop novel strategies and conceptual models. Network theory as well as the development of more advanced neural network topologies, capable of representing complex data-structures, has presented the opportunity to model and analyse the relationships between mathematical concepts from the bottom up. Generative Adversarial Networks build on this foundation, allowing us to develop creative software to manipulate and re-express this knowledge, and has many applications within Interactive and Automated Theorem Proving where both recognising and re-applying knowledge for new problems or situations is necessary to all stages of the proof process.In 1994 the QED Manifesto presented a vision of Mathematics where all proofs are automatically formalised upon their inclusion into a monolithic digital archive. The motivations included: ensuring correctness, addressing organisational issues, improving dissemination and education, as well as enabling meta-analysis. Over two decades later, this vision has not materialised, yet it remains both relevant and achievable.A QED archive was predicated on the parallel construction of a QED-like system, an Interactive Theorem Prover (ITP) which could reduce the labour and technical expertise required to create formal proofs by automating a substantial portion of the process, promoting its adoption by the broader Mathematical community. Because, when contrasted with the conventional mathematical process, contemporary ITPs remain difficult and time consuming to use. Furthermore, most ITPs use different constructivist logics which are more restrictive than classical mathematics, limiting both what a QED-archive could contain and how broadly its entries may be applied.The intended practical contributions of this project would be to improve the proof rate in ITPs by improving how prior work is utilised for new proofs by both human experts and Automated Theorem Provers (ATPs). The ability to generate relevant lemmas and strategies could significantly improve the success rate of ATPs. Specifically, using a network-based approach to this task has the potential to leverage previously unexploited features that could improve performance when combined with conventional techniques as part of an ensemble.There is potential too for this mapping to facilitate a mechanism for interoperability or automated translation of formal proofs between Logics, Software, and Archives, addressing the usability concerns of ITPs. Finally, there is a hard limit to how useful any automated suggestion technique can be without altering the corpus they operate from, finding the best way to organise these libraries is necessary for the continuing improvement of ATPs.