Artifical intelligence and inherent mathematical difficulty
This work addresses foundational questions about the limits of AI in mathematics, but it is incremental as it builds on traditional arguments without presenting new empirical results.
The paper argues that AI methods, despite recent successes in automated theorem proving and related tasks, face inherent limitations due to computability and complexity theory, as they rely on brute-force search and can only handle statements of low logical complexity.
This paper explores the relationship of artificial intelligence to the task of resolving open questions in mathematics. We first present an updated version of a traditional argument that limitative results from computability and complexity theory show that proof discovery is an inherently difficult problem. We then illustrate how several recent applications of artificial intelligence-inspired methods -- respectively involving automated theorem proving, SAT-solvers, and large language models -- do indeed raise novel questions about the nature of mathematical proof. We also argue that the results obtained by such techniques do not tell against our basic argument. This is so because they are embodiments of brute force search and are thus capable of deciding only statements of low logical complexity.