00:00:00 / 00:00:00

Recursive inequalities in applied proof theory

By Thomas Powell

Appears in collection : Type Theory, Constructive Mathematics and Geometric Logic / Théorie des types, mathématiques constructives et logique géométrique

Applied proof theory is an area of research that uses ideas and techniques from proof theory to produce new results in 'mainstream' mathematics and computer science. While the field has historical roots in Hilbert's program, where it aligns with the much broader effort to give a computational meaning to mathematical proofs, its emergence as a powerful area of applied logic only started in the early 2000s with the research of Kohlenbach and his collaborators. This talk aims to accomplish two things. Firstly, I seek to give a brief overview of the main ideas behind applied proof theory without assuming any prior background in the area. Secondly, within this context, I want to present some recent results which have focused on abstract convergence properties of sequences of real numbers that satisfy certain recursive inequalities. I argue that recursive inequalities present us with a unifying framework for viewing many convergence proofs in the literature, and propose what I believe to be some fascinating possibilities for future work, involving stochastic convergence, computer formalized mathematics and automated reasoning.

Information about the video

Citation data

  • DOI 10.24350/CIRM.V.20041003
  • Cite this video Powell Thomas (5/2/23). Recursive inequalities in applied proof theory. CIRM. Audiovisual resource. DOI: 10.24350/CIRM.V.20041003
  • URL https://dx.doi.org/10.24350/CIRM.V.20041003


Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow


  • Bookmark videos
  • Add videos to see later &
    keep your browsing history
  • Comment with the scientific
  • Get notification updates
    for your favorite subjects
Give feedback