Theorem Proving in Large Formal Mathematics as an Emerging AI Field

TL;DR

This paper discusses the emerging field of AI-driven theorem proving in large formal mathematics, highlighting recent developments, historical context, and future research directions in combining AI with automated theorem proving tools.

Contribution

It connects recent AI/ATP systems with historical efforts and discusses the potential of formal mathematics as a new semantic AI research area.

Findings

Linking formal mathematics with ATP tools advances automated reasoning.

Historical comparison with Otter and QED projects highlights progress.

Future research directions are outlined for AI in formal mathematics.

Abstract

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.