Towards the automatic mathematician (Q2055841)

The authors in this paper examine recent progress in the field of neural theorem proving and their goal to create an artificial mathematician. They acknowledge the challenges that lie ahead, but highlight that even partial success in this mission could bring substantial benefits to the formal methods community and related areas such as verification, program synthesis, and natural language understanding. A survey of AI researchers conducted in 2018 estimated that machines would be capable of routinely proving mathematical theorems in top journals by the 2060s. However, the authors believe that recent breakthroughs in deep learning suggest that the development of an intelligent artificial mathematician may occur much sooner. Despite ongoing challenges, the authors are optimistic about the potential for future success in this field. For the entire collection see [Zbl 1475.68026].