Artifical intelligence and inherent mathematical difficulty

TL;DR

This paper examines how artificial intelligence impacts mathematical problem-solving, highlighting its limitations due to inherent computational complexity and demonstrating that current AI methods are mainly brute-force approaches suited for low-complexity problems.

Contribution

It provides an updated argument on the inherent difficulty of proof discovery and analyzes recent AI applications, clarifying their capabilities and limitations in mathematical reasoning.

Findings

AI methods are limited to low logical complexity problems

Computability and complexity theory impose fundamental limits on proof discovery

Recent AI techniques do not challenge the inherent difficulty of mathematical proof

Abstract

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.