![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Thursday 22 February 2024, 17:00-18:00
Experiences with Isabelle/HOL: Formalising Real Algebraic Geometry
- đ¤ Speaker: Artie Khovanov (University of Cambridge), Michael Nedzelsky (Diffblue Ltd) and Dr Wenda Li (University of Edinburgh)
- đ Date & Time: Thursday 22 February 2024, 17:00 - 18:00
- đ Venue: MR14 Centre for Mathematical Sciences
Abstract
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
Series This talk is part of the Formalisation of mathematics with interactive theorem provers series.
Included in Lists
- All CMS events
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- CMS Events
- Department of Computer Science and Technology talks and seminars
- DPMMS info aggregator
- DPMMS lists
- DPMMS Lists
- DPMMS Pure Maths study groups
- Formalisation of mathematics with interactive theorem provers
- Hanchen DaDaDash
- Interested Talks
- Martin's interesting talks
- MR14 Centre for Mathematical Sciences
- School of Physical Sciences
- School of Technology
- Trust & Technology Initiative - interesting events
- yk449
Note: Ex-directory lists are not shown.