BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalised Mathematics: Obstacles and Achievements - Professor Law
 rence Paulson - Department of Computer Science and Technology
DTSTART:20221123T150500Z
DTEND:20221123T155500Z
UID:TALK182654@talks.cam.ac.uk
CONTACT:Ben Karniely
DESCRIPTION:The practice of formalising mathematics is starting to attract
  the attention of mathematicians themselves. The main motivation is an awa
 reness that mathematicians regularly make serious errors\, some of which g
 o undetected. But is formalised mathematics at all a realistic possibility
 ? By now a great body of mathematics has been formalised. Unfortunately\, 
 rather little of it approaches the sophistication of modern research mathe
 matics. Moreover\, formalised proofs are typically unreadable and require 
 lengthy blocks of code to prove obvious facts. Researchers are now formali
 sing more advanced mathematical concepts\, but much more remains to be don
 e.\n\nLink to join virtually: https://zoom.us/j/98901725392?pwd=UWNVZVFTcV
 QxL2JkS0V1WVBoelBuUT09\n\nA recording of this talk is available at the fol
 lowing link: https://www.cl.cam.ac.uk/seminars/wednesday/video/
LOCATION:Lecture Theatre 1\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR