BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Computer Algebra and the Formalisation of New Mathematics - Lawren
 ce Paulson (University of Cambridge)
DTSTART:20241121T170000Z
DTEND:20241121T180000Z
UID:TALK222775@talks.cam.ac.uk
CONTACT:Jonas Bayer
DESCRIPTION:Although people have sought to integrate computer algebra with
  theorem proving since the 1990s\, none of today’s proof assistants clai
 m to offer such an integration. However\, Isabelle is capable of some basi
 c computer algebra tasks\, including symbolic differentiation (and hence s
 ymbolic integration via the FTC)\, deductive limit finding and exact arbit
 rary-precision real arithmetic. These facilities will be presented alongsi
 de their application to formalising last year’s celebrated result of an 
 exponentially improved upper bound for Ramsey numbers.\n\nSlides: https://
 www.cl.cam.ac.uk/~lp15/papers/Alexandria/SC-Square-2024.pdf\n\nRecording: 
 https://youtu.be/HeQKT6OeIX4
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR