Abstract:  Since the launch of ChatGPT about two years ago, GPT-like "foundation models" in AI have become a common tool. Such models continue to rapidly improve, including in their reasoning capabilities. Meanwhile, over the last few years Interactive Theorem Provers, especially Lean and its library Mathlib, are entering the mainstream of mathematics. Alongside these more dramatic advances, mathematical software such as Computer Algebra Systems as well as Symbolic AI based Automated Theorem Provers have continued to advance rapidly.

         The capabilities of Generative AI, Interactive Theorem Provers, Symbolic AI and Mathematical software complement each other, showing great promise for tools to help in mathematical discovery. In the longer run these show potential for fully autonomous mathematical discovery.

         In this talk I will discuss examples of what has been done with such systems, including hybrid ones, and the potential for their use. I will also discuss the possibility of autonomous systems and their ramifications.

About the speaker: Dr. Siddhartha Gadgil is a Professor in the Department of Mathematics at the Indian Institute of Science. His research interests are in (Low-dimensional) Topology and related areas, including Geometric group theory, Riemannian geometry and Metric Geometry (and its relation to Probability Theory). More recently, he is focused on Automated Theorem Proving, i.e., trying to get computers to do mathematics.