University of Birmingham > Talks@bham > Lab Lunch > Specker sequences and their relevance to Proof Mining

Specker sequences and their relevance to Proof Mining

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

If you have a question about this talk, please contact Anupam Das.

The Proof Mining project aims to see what quantitative information can be extracted from proofs using techniques from proof theory. A classic example of this is the following: Given a proof that a sequence converges, can we extract a rate of convergence? In this talk, I will present some important theoretical results in this direction. Firstly, I will outline E. Specker’s proof that there exist convergent sequences of computable numbers which don’t have a rate of convergence. However, not all hope is lost! Applying the classical functional interpretation to the statement of Cauchy convergences yields what is known as a ‘rate of metastability’ which, like a rate of convergence, provides extra quantitative information about the convergence of a sequence. I will explain what this is, and then give some new examples from work in progress where both rates of convergence and rates of metastability have been extracted from convergence proofs. Lastly, I will outline some ongoing work on formalising concepts from proof mining and computable analysis in the Lean proof assistant, where in particular I have formalised Specker’s construction, defined the concepts of computable rates of convergence and metastability, and I have proved basic lemmas related to how they interact with Cauchy convergence as well as each other.

==== Zoom details ====

Meeting ID: 818 7333 5084 Passcode: 217

This talk is part of the Lab Lunch series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.