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 <andrei.h.pope...@gmail.com> 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. _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
