Re: [Caml-list] Jeremy Avigad to give this year's LMS/BCS-FACS Evening Seminar -- 6 November 2025, online via Zoom

[Andrei Popescu <andrei.h.popescu@gmail.com>]

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://www.andrew.cmu.edu/user/avigad/

Registration (for access to the Zoom link):
https://www.lms.ac.uk/events/lms-bcs-facs-seminar-jeremy-avigad

Best wishes,
Andrei


On Wed, Oct 8, 2025 at 3:22 AM Andrei Popescu
<andrei.h.popescu@gmail.com> 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://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.