Theorem Proving in Large Formal Mathematics as an Emerging AI Field
This work addresses the problem of automating theorem proving in formal mathematics for AI researchers, but it is incremental as it builds on prior projects like Quaife's and QED.
The paper connects a large corpus of formal mathematics with automated theorem proving tools, arguing that this creates an emerging semantic AI field, and relates this to earlier large-scale developments like the QED project.
In the recent years, we have linked a large corpus of formal mathematics with automated theorem proving (ATP) tools, and started to develop combined AI/ATP systems working in this setting. In this paper we first relate this project to the earlier large-scale automated developments done by Quaife with McCune's Otter system, and to the discussions of the QED project about formalizing a significant part of mathematics. Then we summarize our adventure so far, argue that the QED dreams were right in anticipating the creation of a very interesting semantic AI field, and discuss its further research directions.