Re: [Hol-info] LMS/BCS-FACS online talk by Lawrence Paulson, 15 January 2024

[Andrei P. <and...@gm...>]

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


On Mon, Jan 8, 2024 at 11:00 AM Andrei Popescu
<and...@gm...> wrote:
>
> 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.