BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Experiences with Isabelle/HOL: Formalising Real Algebraic Geometry
  - Artie Khovanov (University of Cambridge)\, Michael Nedzelsky (Diffblue 
 Ltd) and Dr Wenda Li (University of Edinburgh)
DTSTART:20240222T170000Z
DTEND:20240222T180000Z
UID:TALK211648@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:The Isabelle/HOL interactive theorem prover has multiple frame
 works for formalising abstract algebra: one library which relies on typecl
 asses\, and another\, better suited to formalising algebra\, which makes n
 o use of them. In this talk\, we discuss the experience of formalising mat
 erial in real algebraic geometry – real closed fields\, Thom encoding an
 d Puiseux series – in the latter framework. We explore the strengths and
  weaknesses of the available automation\, as well as the feasibility of tr
 ansferring results from one library to the other.\n\n—-\n\nWATCH ONLINE 
 HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=
 1 Meeting ID: 370 771 279 261 Passcode: iCo7a5
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR