The standard reference for proof mining is the monograph of Ulrich Kohlenbach:

• U. Kohlenbach, Applied proof theory: Proof interpretations and their use in mathematics. Springer Monographs in Mathematics, Springer, 2008.

Surveys

The following surveys and expository papers, also by Ulrich Kohlenbach, cover recent applications:

• U. Kohlenbach, Recent progress in proof mining in nonlinear analysis. Journal of Applied Logics – IfCoLog Journal of Logics and their Applications, Vol. 10, Issue 4, 3361–3410, 2017.

• U. Kohlenbach, Proof-theoretic methods in nonlinear analysis. In: B. Sirakov, P. Ney de Souza, M. Viana (eds.), Proceedings of the International Congress of Mathematicians 2018 (ICM 2018), Vol. 2 (pp. 61–82). World Scientific, Singapore, 2019.

• U. Kohlenbach, Local formalizations in nonlinear analysis and related areas and proof-theoretic tameness. In: P. Weingartner, H.-P. Leeb (eds.), Kreisel’s Interests. On the Foundations of Logic and Mathematics (pp. 45–61). College Publications, 2020.

• U. Kohlenbach, Kreisel’s ‘shift of emphasis’ and contemporary proof mining. Studies in Logic Vol. 16, No. 3, pp. 1–35, 2023.

This Oberwolfach report of Laurențiu Leuștean, which surveys his 2000s research, contains a reasonably self-contained introduction to the ideas of proof mining:

• L. Leuștean, Proof mining in metric fixed point theory and ergodic theory. Oberwolfach Preprints OWP 2009-05, Mathematisches Forschungsinstitut Oberwolfach, 2009.

The following notes support the proof mining tutorial delivered by Andrei Sipoș at Logic Colloquium 2024:

• A. Sipoș, An exploration of proof mining. 2024.

Talks

• U. Kohlenbach, Proof Interpretations and Their Application to Current Mathematics, 2011.

• U. Kohlenbach, Proof Mining and the ‘Lion-Man’ Game, 2020.

• T. Powell, Recursive inequalities in applied proof theory, 2023.

• U. Kohlenbach, Proof mining: recent developments, 2023.

Blog posts

The following series of Proof Theory Blog articles by Andrei Sipoș introduces proof mining to the working logician:

• “What proof mining is about, Part I”

• “What proof mining is about, Part II: Structures and metatheorems”

• “What proof mining is about, Part III: The Heroic Age of Unwinding Proofs”

• “What proof mining is about, Part IV: Kohlenbach & friends”

Slides

• U. Kohlenbach, Local proof-theoretic foundations and proof-theoretic tameness in ordinary mathematics, Retiring Presidential Address, ASL Logic Colloquium 2019, Prague, 2019.

• A. Sipoș, Advances in proof mining (University of Bucharest lectureship competition scientific talk; summary of author’s research 2015-2020), 2020.

• T. Powell, Proof Mining lectures (1, 2, 3, 4), Nordic Logic Summer School (NLS ’22), University of Bergen, 2022.

• U. Kohlenbach, Proof Mining: Extraction of Information from Proofs, course given at 6th International Proof Society Summer School, Birmingham, 2024.

Proof Mining Seminar

The Proof Mining Seminar webpage is currently hosted by the Institute for Logic and Data Science, Bucharest.

Theses

• U. Kohlenbach, Theorie der majorisierbaren und stetigen Funktionale und ihre Anwendung bei der Extraktion von Schranken aus inkonstruktiven Beweisen: Effektive Eindeutigkeitsmodule bei besten Approximationen aus ineffektiven Eindeutigkeitsbeweisen, PhD thesis, Frankfurt, 1990.

• P. Oliva, Proof Mining in Subsystems of Analysis, PhD thesis, Aarhus, 2003.

• P. Gerhardy, Applications of Proof Interpretations, PhD thesis, Aarhus, 2006.

• B. Lambov, Topics in the Theory and Practice of Computable Analysis, PhD thesis, Aarhus, 2006.

• E. Briseid, On Rates of Convergence in Metric Fixed Point Theory, PhD thesis, Darmstadt, 2009.

• P. Engrácia, Proof-theoretical studies on the bounded functional interpretation, PhD thesis, Lisbon, 2009.

• J. Gaspar, Proof interpretations: theoretical and practical aspects, PhD thesis, Darmstadt, 2012.

• A. Kreuzer, Proof mining and combinatorics: Program extraction for Ramsey’s theorem for pairs, PhD thesis, Darmstadt, 2012.

• T. Powell, On Bar Recursive Interpretations of Analysis, PhD thesis, London, 2013.

• D. Körnlein, Quantitative Analysis of Iterative Algorithms in Fixed Point Theory and Convex Optimization, PhD thesis, Darmstadt, 2016.

• A. Koutsoukou-Argyraki, Proof Mining for Nonlinear Operator Theory, PhD thesis, Darmstadt, 2017.

• A. Sipoș, Contributions to proof mining, PhD thesis, Bucharest, 2017.

• P. Pinto, Proof mining with the bounded functional interpretation, PhD thesis, Lisbon, 2019.

• N. Pischke, Proof-Theoretical Aspects of Nonlinear and Set-Valued Analysis, PhD thesis, Darmstadt, 2023.

• H. Cheval, Proof mining and applications to optimization and nonlinear analysis, PhD thesis, Bucharest, 2024.

The Proof Mining Bibliography

The Proof Mining Bibliography was initiated by Nicholas Pischke and is an attempt to collect some of the many relevant references for works from and around the area of proof mining. For simplicity, the focus is (initially) on applications in analysis and on applications using functional interpretations. Due to the breadth of this goal, the list will presumably always be incomplete. You can access it here.