Augmenting the human mathematician
In this article we consider important developments in artificial intelligence within automated andinteractive theorem provers (ATP/ITP). Our focus is to describe and analyze key challenges for interactive theorem provers in mainstream mathematical practice. Our broader research program is motivated...
| Main Authors: | , , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Math-AI
2021
|
| _version_ | 1797052976002498560 |
|---|---|
| author | Sørensen, HK Johansen, MW Hoekzema, R Breman, H |
| author_facet | Sørensen, HK Johansen, MW Hoekzema, R Breman, H |
| author_sort | Sørensen, HK |
| collection | OXFORD |
| description | In this article we consider important developments in artificial intelligence within automated andinteractive theorem provers (ATP/ITP). Our focus is to describe and analyze key challenges for interactive theorem provers in mainstream mathematical practice. Our broader research program is motivated by studying the functions of visual internal and external representations in human mathematicians and the role of epistemic emotions. These aspects remain gorges to bridge in developing ITPs. But by seeing ITPs as augmenting the human mathematician, we stand to gain the best of two epistemic practices in the form of a hybrid — a centaur. |
| first_indexed | 2024-03-06T18:38:01Z |
| format | Conference item |
| id | oxford-uuid:0bf3be91-2928-480d-b25d-f1ca54ebb449 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T18:38:01Z |
| publishDate | 2021 |
| publisher | Math-AI |
| record_format | dspace |
| spelling | oxford-uuid:0bf3be91-2928-480d-b25d-f1ca54ebb4492022-03-26T09:32:07ZAugmenting the human mathematicianConference itemhttp://purl.org/coar/resource_type/c_5794uuid:0bf3be91-2928-480d-b25d-f1ca54ebb449EnglishSymplectic ElementsMath-AI2021Sørensen, HKJohansen, MWHoekzema, RBreman, HIn this article we consider important developments in artificial intelligence within automated andinteractive theorem provers (ATP/ITP). Our focus is to describe and analyze key challenges for interactive theorem provers in mainstream mathematical practice. Our broader research program is motivated by studying the functions of visual internal and external representations in human mathematicians and the role of epistemic emotions. These aspects remain gorges to bridge in developing ITPs. But by seeing ITPs as augmenting the human mathematician, we stand to gain the best of two epistemic practices in the form of a hybrid — a centaur. |
| spellingShingle | Sørensen, HK Johansen, MW Hoekzema, R Breman, H Augmenting the human mathematician |
| title | Augmenting the human mathematician |
| title_full | Augmenting the human mathematician |
| title_fullStr | Augmenting the human mathematician |
| title_full_unstemmed | Augmenting the human mathematician |
| title_short | Augmenting the human mathematician |
| title_sort | augmenting the human mathematician |
| work_keys_str_mv | AT sørensenhk augmentingthehumanmathematician AT johansenmw augmentingthehumanmathematician AT hoekzemar augmentingthehumanmathematician AT bremanh augmentingthehumanmathematician |