Date:
Thursday, 22 February, 2024 - 17:00 to 18:00
Speaker:
Artie Khovanov (University of Cambridge), Michael Nedzelsky (Diffblue Ltd) and Dr Wenda Li (University of Edinburgh)
Venue:
MR14 Centre for Mathematical Sciences
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
Seminar series:
Formalisation of mathematics with interactive theorem provers
