Mapping and Re-applying Mathematical Knowledge in Mechanical Theorem Proving

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

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.