  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.
