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
