1

Introduction

Artificial intelligence (AI) is useful in various research disciplines, and its applicability to mathematical research has drawn growing interest in recent years. For example, Davies and colleagues (2021) used AI to help produce two meaningful contributions to mathematics: one in representation theory, producing a proof for a conjecture that had remained unsolved for over 40 years, and one in topology, connecting the algebraic and geometric structure of knots in a new way. These contributions are just two of many that demonstrate that AI has the potential to aid new mathematical discoveries. Particularly as the amount of data available grows beyond what any person can study, AI can be useful in its power to identify patterns in data.

Davies and colleagues (2021) explained that machine learning (ML), a type of AI, can be a powerful tool in refining relationships between properties. Traditionally, this part of the mathematical research process requires the mathematician’s intuition; ML can help guide intuition by quickly testing whether a relationship may be worth exploring further. More generally, ML can assist high-level idea generation in mathematics. Additionally, symbolic AI, which is another type of AI distinct from ML, can be useful to mathematics research as well. Symbolic automated reasoning tools such as first-order theorem provers embody a complementary approach to using AI to assist mathematical reasoning, and they can be especially useful in formalizing mathematics—essentially digitizing mathematics in a computer proof assistant—and can ultimately open up new avenues for mathematical research.

Mathematical reasoning is a central aspect of human intelligence that plays an important role in knowledge discovery. In the past few decades, the mathematics and computer science communities have contributed to research on how AI may assist mathematical reasoning, whether that is through the use of ML for guiding idea generation or finding counterexamples to conjectures, the use of symbolic AI for formalizing mathematics, or other ways entirely. Recent technical advances have led to a surge of interest in this domain from the mathematical and computer science communities, as well as from the AI community.

WORKSHOP OVERVIEW

Sponsored by the National Science Foundation (NSF), the National Academies of Sciences, Engineering, and Medicine’s Board on Mathematical Sciences and Analytics convened a 3-day public virtual workshop on June 12–14, 2023, to bring together stakeholders to discuss the state of the art and current challenges and opportunities to advance research in using AI for mathematical reasoning (see Box 1-1 for the workshop’s statement of task).

At the beginning of the workshop, David Manderscheid, director of the Division of Mathematical Sciences (DMS) at NSF, and Dilma Da Silva, director of the Division on Computing and Communication Foundations (CCF) at NSF, gave brief remarks on NSF’s interest in AI to assist mathematical reasoning. Manderscheid explained that AI is a priority at NSF, and the application of AI to mathematics in particular has recently garnered attention. He identified DMS’s interest in both research and education and expressed that AI has the potential to transform the way mathematics research is conducted. Da Silva emphasized CCF’s interest in formal methods and verification of software and hardware as well as AI, and she noted a connection between elements of the workshop and NSF’s larger vision.

Invited workshop speakers included mathematicians and computer scientists, including researchers working in areas such as interactive theorem proving, automated reasoning, formal methods, type theory, and AI and ML. The workshop began with an overview and discussion of case studies, leading to sessions later in Day 1 and throughout Day 2 that explored various challenges and barriers to the adoption of AI for mathematical reasoning. Speakers presenting on Day 3 discussed technical advances required to widen the adoption and roles for stakeholders to advance AI for mathematical reasoning.

ORGANIZATION OF THIS WORKSHOP PROCEEDINGS

Chapter 2 presents an overview of the history, state of the art, and potential futures for using AI to assist mathematical reasoning. Chapter 3 highlights case studies of AI assisting mathematical reasoning as well as case studies in proof verification and checking. Chapter 4 details several challenges and barriers to the adoption of AI for mathematical reasoning, including both institutional and technical challenges. Chapter 5 describes past and potential future research advances in proof verification and AI for mathematical reasoning, particularly exploring synergies between the two, and Chapter 6 details a panel discussion on roles for stakeholders in supporting the advancement of using AI for mathematical reasoning. Finally, Chapter 7 offers key themes underlying the workshop presentations and discussions.

This proceedings was prepared by the workshop rapporteur as a factual summary of what occurred at the workshop. The workshop planning committee’s role was limited to organizing and convening the workshop (see Appendix A for the workshop agenda and Appendix B for biographical sketches of the workshop planning committee members). The views expressed in this proceedings are those of the individual workshop participants and do not necessarily represent the views of

the participants as a whole, the planning committee, or the National Academies.

REFERENCE