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
=== Hybrid talk ===
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1
Meeting ID: 871 4336 5195
Passcode: 541180
