Email Gateway (Jan 08 2024 at 11:00): Email Gateway (Jan 08 2024 at 11:00):From: Andrei Popescu <andrei.h.popescu@gmail.com>
Dear all,
Next week there will be an online talk (via zoom) by Lawrence Paulson
on a topic that is likely to be of interest to quite a few people on
these lists. Please note the information about registration below.
Best wishes,
Andrei
Information: https://www.bcs.org/events-calendar/2024/january/webinar-formalising-21st-century-mathematics/
Date/Time: 15 January 2024, 4-6pm GMT
Speaker: Lawrence C. Paulson FRS, University of Cambridge
Web: https://www.cl.cam.ac.uk/~lp15/
Registration: https://www.lms.ac.uk/events/lms-bcs-facs-seminar-2024
Title: Formalising 21st-Century Mathematics
Abstract: The formalisation of mathematics is an ongoing process that
arguably started as early as the 19th century, intensified with the
foundational crisis at the start of the 20th century, and since the
1970s has been conducted with the help of computers. Recent decades
have seen the machine formalisation of lengthy and technically
complicated proofs, but some have argued that even these were not
representative of modern mathematics. Recent achievements by a number
of different groups are starting to challenge this scepticism. The
speaker will outline some of these, while also noting some of the
remaining trouble spots.
Biography: Lawrence Paulson FRS is an American computer scientist. He
is a Professor of Computational Logic at the University of Cambridge
Computer Laboratory and a Fellow of Clare College, Cambridge. He is
best known for the cornerstone text on the programming language ML, ML
for the Working Programmer. His research is based around the
interactive theorem prover Isabelle, which he introduced in 1986. He
has worked on the verification of cryptographic protocols using
inductive definitions, and he has also formalised the constructible
universe of Kurt Gödel. Recently he has built a new theorem prover,
MetiTarski, for real-valued special functions.
Email Gateway (Jan 08 2024 at 12:47):From: Andrei Popescu <andrei.h.popescu@gmail.com>
Dear colleagues,
Another note: This talk will be recorded and made available on youtube
(I will come back with the link). I would like to apologise to those
of you attending CPP -- when scheduling this (which happened a while
ago) I lost sight of the overlap with CPP. :-(
Best wishes,
Andrei
Last updated: Apr 29 2024 at 01:08 UTC