Mapping and Re-applying Mathematical Knowledge in Mechanical Theorem Proving

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