# Artifical intelligence and inherent mathematical difficulty

arXiv: https://arxiv.org/abs/2408.03345 · HTML: https://mlsanity.com/paper/2408.03345/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 9 of its 103 references that are in the map.
- First posted on arXiv 1 Aug 2024.

## Builds on (most cited first, 9 of 9)

- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer](https://mlsanity.com/paper/1605.00723/) (2016)
- [Alien Coding](https://mlsanity.com/paper/2301.11479/) (2023)
- [Learning Program Synthesis for Integer Sequences from Scratch](https://mlsanity.com/paper/2202.11908/) (2022)
- [ATG: Benchmarking Automated Theorem Generation for Generative Language Models](https://mlsanity.com/paper/2405.06677/) (2024)
- [The Packing Chromatic Number of the Infinite Square Grid is 15](https://mlsanity.com/paper/2301.09757/) (2023)
- [Happy Ending: An Empty Hexagon in Every Set of 30 Points](https://mlsanity.com/paper/2403.00737/) (2024)
- [Developments in Formal Proofs](https://mlsanity.com/paper/1408.6474/) (2014)
- [A Mathematical Benchmark for Inductive Theorem Provers](https://mlsanity.com/paper/2304.02986/) (2023)

## Abstract (arXiv)

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.