Mailing list for all users of the OCaml language and system.
 help / color / mirror / Atom feed
From: Andrei Popescu <andrei.h.popescu@gmail.com>
To: caml-list@inria.fr, categories@mta.ca, haskell@haskell.org,
	 haskell-cafe@haskell.org, hol-info@lists.sourceforge.net,
	 acl2@utlists.utexas.edu
Subject: Re: [Caml-list] Jeremy Avigad to give this year's LMS/BCS-FACS Evening Seminar: "Mathematics in the Age of AI" -- 6 November 2025, online via Zoom
Date: Mon, 3 Nov 2025 01:56:23 +0000	[thread overview]
Message-ID: <CAACfPHpFmQg_ZN6Ys5ENA+3PzxG1aoG=pftonOv2j67TwbiFdQ@mail.gmail.com> (raw)
In-Reply-To: <CAACfPHraope1LjHY6UZ5g+Wq2T7-uBuX9qMWDo4CaR-KjJYhFg@mail.gmail.com>

Dear Colleagues,

A brief reminder that Jeremy’s talk is coming up soon. Details are below.

Best wishes,
Andrei

On 08/10/2025 04:22, Andrei Popescu 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
> Registration (for access to the Zoom link):
> https://www.lms.ac.uk/events/lms-bcs-facs-seminar-jeremy-avigad
> Talk title: Mathematics in the Age of AI
> Speaker: Jeremy Avigad (Carnegie Mellon University)
> Jeremy’s website: https://www.andrew.cmu.edu/user/avigad/
>
> 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.

  reply	other threads:[~2025-11-03  1:56 UTC|newest]

Thread overview: 4+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2025-10-08  2:22 [Caml-list] Jeremy Avigad to give this year's LMS/BCS-FACS Evening Seminar " Andrei Popescu
2025-10-08 18:32 ` Andrei Popescu
2025-11-03  1:56   ` Andrei Popescu [this message]
2025-11-03  2:45     ` [Caml-list] LMS Computer Science Colloquium 2025: Combinatorics and Computing, 9 Dec. 2025, De Morgan House, London, UK & " Andrei Popescu

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to='CAACfPHpFmQg_ZN6Ys5ENA+3PzxG1aoG=pftonOv2j67TwbiFdQ@mail.gmail.com' \
    --to=andrei.h.popescu@gmail.com \
    --cc=acl2@utlists.utexas.edu \
    --cc=caml-list@inria.fr \
    --cc=categories@mta.ca \
    --cc=haskell-cafe@haskell.org \
    --cc=haskell@haskell.org \
    --cc=hol-info@lists.sourceforge.net \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox