Center for Cyber-Social Dynamics Welcomes Guest Speaker Presenting on the Challenges in the use of AI in Mathematical Proofs

Faculty leadership at KU’s Center for Cyber-Social Dynamics (CCSD) will welcome a guest speaker from the National Autonomous University of Mexico (UNAM) in June. Dr. Nancy Abigail Nunez will present her research on the prospect of automating mathematical discovery: Challenges in the use of AI in mathematical proofs. The presentation will take place in the executive conference room (Rm. 246) on Friday, June 13, at Nichols Hall on KU’s West District. See the full abstract below.

Nunez received her doctoral degree in philosophy from UNAM, where her areas of study were epistemology, philosophical logic, and logic. Her areas of concentration are philosophy of cognitive sciences, philosophy of math and philosophy of languages. She earned her master’s degree in philosophy of science from UNAM and a master’s degree in philosophy, sciences, and values from the University of the Basque Country in Spain.

CCSD, part of KU’s Institute for Information Sciences (I2S), is focused on the interaction between internet technologies and society.  Research initiatives focus on understanding the psychological, social, cultural, and political effects of technology. Their work brings expertise from the humanities and social sciences into collaborative research with engineering and design.

This presentation is part of what is expected to eventually be a formal collaboration between CCSD and UNAM.

Abstract:

Proof discovery in mathematics has been the pride of mathematicians since the early days of the discipline. Due to the crucial role of proofs in mathematics, various values have been attributed to them: proofs have been described as having explanatory, aesthetic, or motivational value. But even if mathematical proofs are so valuable, proving a mathematical statement is not easy. The history of mathematics and the experiences of mathematicians attest to the difficulty of discovering proofs. Many seem to believe that the progress of Artificial Intelligence (AI) will be a game changer, enabling the automated discovery of mathematical proofs and making the task of proving mathematical statements easier, if not effortless. But is it actually possible to fully automate the discovery of mathematical proofs?  This research aims to investigate the challenges of automating the discovery of mathematical proofs, taking into account computational complexity constraints. Such challenges to automating mathematical proofs have epistemological implications since proof is often considered akin to epistemic justification within the context of mathematical reasoning and knowledge. Since both human and artificial cognitive agents have bounded cognitive resources, the results of computational complexity theory set limits on what an agent can compute and get to know after the computation.