Proof mining
Encyclopedia
In proof theory
, a branch of mathematical logic
, proof mining (or unwinding) is a research program that analyzes formalized proofs, especially in analysis
, to obtain explicit bounds or rates of convergence
from proofs that, when expressed in natural language, appear to be nonconstructive.
This research has led to improved results in analysis obtained from the analysis of classical proofs.
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
, a branch of mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, proof mining (or unwinding) is a research program that analyzes formalized proofs, especially in analysis
Mathematical analysis
Mathematical analysis, which mathematicians refer to simply as analysis, has its beginnings in the rigorous formulation of infinitesimal calculus. It is a branch of pure mathematics that includes the theories of differentiation, integration and measure, limits, infinite series, and analytic functions...
, to obtain explicit bounds or rates of convergence
Rate of convergence
In numerical analysis, the speed at which a convergent sequence approaches its limit is called the rate of convergence. Although strictly speaking, a limit does not give information about any finite first part of the sequence, this concept is of practical importance if we deal with a sequence of...
from proofs that, when expressed in natural language, appear to be nonconstructive.
This research has led to improved results in analysis obtained from the analysis of classical proofs.