Experiences with Isabelle/HOL: Formalising Real Algebraic Geometry

Add to your list(s) Download to your calendar using vCal

• Artie Khovanov (University of Cambridge), Michael Nedzelsky (Diffblue Ltd) and Dr Wenda Li (University of Edinburgh)
• Thursday 22 February 2024, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

The Isabelle/HOL interactive theorem prover has multiple frameworks for formalising abstract algebra: one library which relies on typeclasses, and another, better suited to formalising algebra, which makes no use of them. In this talk, we discuss the experience of formalising material in real algebraic geometry – real closed fields, Thom encoding and Puiseux series – in the latter framework. We explore the strengths and weaknesses of the available automation, as well as the feasibility of transferring results from one library to the other.

—-

WATCH ONLINE HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 Passcode: iCo7a5

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.