Webinar: LMS/BCS-FACS Seminar with Jeremy Avigad (Carnegie Mellon University)

New technologies for reasoning and discovery are bound to have a profound effect on mathematical practice. Proof assistants are already changing the nature of collaboration, communication, and curation of mathematical knowledge. Automated reasoning tools are used to find mathematical objects with specified properties or rule out their existence, and to decide or verify mathematical claims. Machine learning and neural methods can discover patterns in mathematical data, explore complex mathematical spaces, and generate mathematical objects of interest.

Neurosymbolic theorem provers, now capable of solving the most challenging competition problems, combine aspects of all of these technologies.

It is helpful to keep in mind that the phrase "AI for mathematics" encompasses several distinct technologies that overlap and interact in interesting ways. In this talk, I will survey the landscape, describe a few landmark applications to mathematics, and encourage you to join me in thinking about how mathematicians and computer scientists can collaborate to guide mathematics through this era of technological change.