![[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 21 November 2024, 17:00-18:00
Computer Algebra and the Formalisation of New Mathematics
- 👤 Speaker: Lawrence Paulson (University of Cambridge)
- 📅 Date & Time: Thursday 21 November 2024, 17:00 - 18:00
- 📍 Venue: MR14 Centre for Mathematical Sciences
Abstract
Although people have sought to integrate computer algebra with theorem proving since the 1990s, none of today’s proof assistants claim to offer such an integration. However, Isabelle is capable of some basic computer algebra tasks, including symbolic differentiation (and hence symbolic integration via the FTC ), deductive limit finding and exact arbitrary-precision real arithmetic. These facilities will be presented alongside their application to formalising last year’s celebrated result of an exponentially improved upper bound for Ramsey numbers.
Slides: https://www.cl.cam.ac.uk/~lp15/papers/Alexandria/SC-Square-2024.pdf
Recording: https://youtu.be/HeQKT6OeIX4
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.