Mathematics in the Age of AI (online talk by Avigad next month)

[Joao Marcos]

---------- Forwarded message ---------
From: Andrei Popescu


Dear Colleagues,

I am delighted to announce that this year’s London Mathematical Society
(LMS) / British Computer Society -- Formal Aspects of Computing Science
(BCS-FACS) Evening Seminar will feature Jeremy Avigad as the distinguished
speaker. Registration is free but required in advance.

Date: 6 November 2025
Time: 19:00 (UK time)
Format: Online via Zoom
Talk title: Mathematics in the Age of AI
Jeremy’s website: https://lnkd.in/ep3w-fiB

Registration (for access to the Zoom link) is available here:
https://lnkd.in/eRE-Bb2A

Further details about the talk are included below

Best wishes,
Andrei


Speaker: Jeremy Avigad (Carnegie Mellon University)
Title: Mathematics in the Age of AI

Abstract:
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.

Bio:
Jeremy Avigad is a professor in the Department of Philosophy and the
Department of Mathematical Sciences at Carnegie Mellon University. He is
the director of the Institute for Computer-Aided Reasoning in Mathematics,
a new NSF Mathematical Sciences Research Institute, and the director of the
Hoskinson Center for Formal Mathematics, a research center at Carnegie
Mellon. He has contributed to mathematical logic and the history and
philosophy of mathematics, and he is currently working on applications of
formal methods and AI to mathematics. He serves on the Lean Community Admin
Team and the board of the Lean Focused Research Organization.