[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Dear Colleagues,
Apologies for my earlier message, which included LinkedIn-redirected
links by mistake. I’m resending the seminar info below with the
correct direct links:
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://urldefense.com/v3/__https://www.andrew.cmu.edu/user/avigad/__;!!IBzWLUs!WcprPM6qs9gV-wcStG6JjDMjJeetBhrNgRA9OKVmfm9HqhAn2lMxiHQRP_bM0qxozwyCbaE8jnzDqDfL3A6fJdsue9MT-jCFB60Ig8-1$
Registration (for access to the Zoom link):
https://urldefense.com/v3/__https://www.lms.ac.uk/events/lms-bcs-facs-seminar-jeremy-avigad__;!!IBzWLUs!WcprPM6qs9gV-wcStG6JjDMjJeetBhrNgRA9OKVmfm9HqhAn2lMxiHQRP_bM0qxozwyCbaE8jnzDqDfL3A6fJdsue9MT-jCFB9fRDh8j$
Best wishes,
Andrei
On Wed, Oct 8, 2025 at 3:15 AM Andrei Popescu
<[email protected]> wrote:
>
> 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://urldefense.com/v3/__https://lnkd.in/ep3w-fiB__;!!IBzWLUs!WcprPM6qs9gV-wcStG6JjDMjJeetBhrNgRA9OKVmfm9HqhAn2lMxiHQRP_bM0qxozwyCbaE8jnzDqDfL3A6fJdsue9MT-jCFB79V183m$
>
>
> Registration (for access to the Zoom link) is available here:
> https://urldefense.com/v3/__https://lnkd.in/eRE-Bb2A__;!!IBzWLUs!WcprPM6qs9gV-wcStG6JjDMjJeetBhrNgRA9OKVmfm9HqhAn2lMxiHQRP_bM0qxozwyCbaE8jnzDqDfL3A6fJdsue9MT-jCFBx6Iwikg$
>
>
> 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.
