Automated Theorem Discovery

这个项目代表了一个多阶段项目的第二阶段，其长期目标是模拟人类数学发现过程的很大一部分。这个特定阶段的重点是完全开发和部署自动化定理发现（Automated Theorem Discovery， ATD）系统。通过ATD系统，我们指的是一个自动生成、证明和识别大量数学结果的系统，数学家可能会将这些结果视为定理、引理、推论等（而不是那些尽管可能是真的、但可能不值得记录的结果）。一代又一代的数学家都认识到一点一点、一个定理一个定理地建立数学知识库的好处，因为先前发现的结果往往在发现和证明后续结果时非常有用——甚至可能是必要的。此外，自从现代计算机出现以来，越来越明显的是，自动推理（AR）系统也可以从类似的定理增量积累中受益。对于某些形式化验证问题尤其如此，在这些问题中，最先进的自动化定理证明者可以分派一些——但不是全部——生成的证明义务。剩下的证明只有在某些引理被发现之后才能完成；目前，这项发现必须靠手工完成。因此，我们预计，一个有效而实用的ATD系统将非常有用，不仅对数学家，而且对计算机科学家——特别是那些从事形式验证工作的科学家——也非常有用。事实上，在后一种情况下，我们有支持的证据（以支持信的形式）表明，这样一个系统的潜在回报是巨大的。

This project represents the second stage of a multi-stage project, the long-term goal of which is to emulate a large portion of the human mathematical discovery process. The focus of this particular stage is on fully developing and deploying an Automated Theorem Discovery (ATD) system. By ATD system we mean a system that automatically generates, proves and identifies a significant number of mathematical results which mathematicians are likely to recognize as Theorems, Lemmas, Corollaries, etc. (as opposed to the sorts of results which, true though they might be, would probably not be deemed worthy of recording).Generations of mathematicians have appreciated the benefits of building a mathematical knowledge base bit by bit, Theorem by Theorem, in that previously discovered results often prove quite useful -- perhaps even necessary -- in the discovery and the proof of subsequent results. Moreover, since the advent of the modern computer, it has become increasingly apparent that automated reasoning (AR) systems can likewise benefit from a similar incremental build-up of Theorems. This is especially true for certain formal verification problems, in which state-of-the-art automated theorem provers can dispatch some -- but not all -- of the generated proof obligations. The remaining proofs can only be achieved once certain Lemmas have been discovered; at present, this discovery must be done by hand.We therefore anticipate that an effective and practical ATD system would be very useful, not only to mathematicians, but to computer scientists as well -- particularly those who work in formal verification. Indeed, in the latter case, we have supporting evidence (in the form of letters of support) that the potential payoff for such a system is huge.