Proof mining is the logical analysis of mathematical proofs in order to extract explicit quantitative information. Proof interpretations can extract computable bounds, rates of convergence, rates of metastability, or algorithms from proofs that appear to establish only existence or convergence. The method is used especially in analysis, where the extracted bounds may be uniform over parameters that occur in the original theorem. Proof mining is also called proof unwinding.
For example, let 
be a nondecreasing sequence with 
. Given 
and a function 
, define 
and 
. There is an 
such that
 |
for all integers 
and 
satisfying 
and 
, where 
denotes 
iterations of 
. Otherwise, at each successive starting point 
for 
, the sequence would
increase by at least 
.
Its total increase would then exceed 1, contradicting 
. This explicit finite bound
is a simple instance of a rate of metastability extracted from a qualitative convergence
statement.
