Developing an intuitive automated theorem prover

与Tim Gowers教授（组合学）合作，作为Cantab Capital信息数学研究所的一部分。数学家很少使用证明辅助工具和自动推理工具，通常作为最后的手段。这个项目旨在探索如何改进这些工具，使它们对数学家更有吸引力。我们打算通过构建使用网络技术以类似人类的方式进行推理的系统来实现这一目标。其目的是这个网络应用程序将能够解释它是如何得到一个给定的证明的，所以它的第一个应用程序可能会对本科生的教学辅助有用。从广义上讲，我想开发的系统可以帮助克服这个可用性问题，并使自动定理证明器更好地为数学家工作。为了实现我开发一个直观的自动化定理证明器的目标，我需要完成以下任务：1。将数学知识转化为易于计算的形式。这可以通过手工输入或对现有文本进行语言分析来实现，如[2].2所示。从现有的形式证明中合成自然语言证明。以一种模仿人类证明定理的方式，发展证明定理的逻辑和启发式。创建允许非专业用户直观地操作给定系统的用户界面。以上所有问题我都感兴趣，但范围太大，不适合作为博士项目进行。在产生理论结果方面，我将主要关注(3)。但我也将实施(1)和(2)的现有研究，以及制作用户界面。

Working with Prof Tim Gowers (Combinatorics) as part of the Cantab Capital Institute for the Mathematics of Information.Proof assistants and automated reasoning tools are used sparingly by mathematicians, and usually as a last resort. This project aims to explore how these tools could be improved to make them more appealing to mathematicians. We intend to achieve this by building systems which reason in a human-like way using web technologies. The aim is that this web-app will be able explain how it arrived at a given proof, so the first applications of this are likely to be useful as a teaching aid to undergraduates. In broad terms, I want to develop systems which help to overcome this usability problem and make automated theorem provers work better for mathematicians. To achieve my aim of developing an intuitive automated theorem prover, I will need to complete the following tasks:1. Translation of mathematical knowledge to an easily computable form. This can be achieved either through manual entry or linguistic analysis of existing texts as demonstrated in [2].2. Synthesis of natural language proofs from existing formal proofs.3. Developing logics and heuristics for proving theorems in a way that mimics how a human would prove theorems.4. Creating user interfaces which allow a non-specialist user to intuitively operate the given system.I am interested in all of the above problems, but the scope is too large to be undertaken as a PhD project. In terms of producing theoretical results, I will mainly concern myself with (3). But I will also be implementing existing research on (1) and (2) as well as producing user interfaces.