Artifical intelligence and inherent mathematical difficulty
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913460397277184 |
|---|---|
| author | Dean, Walter Naibo, Alberto |
| author_facet | Dean, Walter Naibo, Alberto |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_03345 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Artifical intelligence and inherent mathematical difficulty Dean, Walter Naibo, Alberto History and Overview Artificial Intelligence Computational Complexity Logic 03B35, 68V05, 68V15, 68T01 F.2.2; F.4.0; I.2.0; I.2.3; K.2 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. |
| title | Artifical intelligence and inherent mathematical difficulty |
| topic | History and Overview Artificial Intelligence Computational Complexity Logic 03B35, 68V05, 68V15, 68T01 F.2.2; F.4.0; I.2.0; I.2.3; K.2 |
| url | https://arxiv.org/abs/2408.03345 |