Mapping and Re-applying Mathematical Knowledge in Mechanical Theorem Proving

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.