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

[Alex Shkotin]

FYI:Even mathematical theories must be formalized.

Alex

---------- Forwarded message ---------
От: Andrei Popescu <andrei.h...@gmail.com>
Date: ср, 8 окт. 2025 г. в 05:15
Subject: [isabelle] Jeremy Avigad to give this year's LMS/BCS-FACS Evening Seminar -- 6 November 2025, online via Zoom
To: cl-isabelle-users <cl-isabe...@lists.cam.ac.uk>, <coq-...@inria.fr>, <lean...@googlegroups.com>, <ag...@lists.chalmers.se>, <p...@csl.sri.com>, <types-a...@lists.seas.upenn.edu>, <f...@cs.nyu.edu>, Announcement list for the South of England Regional Programming Language Seminar (S-REPLS) <sre...@jiscmail.ac.uk>

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.

[Nadin, Mihai]

--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROQqr1COb5CyC0_%3DogYF-HMC7fPzpZombkLf93-CRcPgXg%40mail.gmail.com.

[John F Sowa]

Alex,

Every mathematical theory from ancient times to the present has always been and always will be 100% formal.   Euclid's diagrams were 100% formal specification of the terms in his theories.  Although he stated his proofs in Greek sentences, every term in those sentences was formally defined by the diagrams.  And every Greek sentence had exactly one and only one interpretation. 

The theorems and proofs were stated so precisely, that the mapping to and from any so called formal notation was trivial.   It added nothing to the understanding.

Furthermore, everything implemented on a digital coputer is 100% formal.  But the methods used by the humans may be so incompletely specified, that the humans don't fully understand how the formal operations work.

But that lack of understanding does not imply that the computing system is doing something informal.  It just means that the people who designed the system don't know how it works.

John

 

---

From: "Alex Shkotin" <alex.s...@gmail.com>

[Chris Partridge]

John: The theorems and proofs were stated so precisely, that the mapping to and from any so called formal notation was trivial.   It added nothing to the understanding.

Furthermore, everything implemented on a digital coputer is 100% formal.  But the methods used by the humans may be so incompletely specified, that the humans don't fully understand how the formal operations work.

👍👍

--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/ba98f346f0e64a3ba8f9ff4fc8fe965c%402499de8d8c4248abb862f52a54634468.