# Proof Mining

**Origin.** Kreisel, Kohlenbach (1990s-present). Extract computational content from classical proofs. Functional interpretations. Quantitative results. Applied proof theory.

**Models.** Classical proofs contain constructive content. Functional interpretation extracts it. Bounds and algorithms. Mathematics applications.

**Formalism.**

*Goal:*
Classical proof of ∀x∃y.A(x,y).
Extract: bound/algorithm for y given x.
Quantitative content.
Effective existence.

*Monotone functional interpretation:*
Variant of Dialectica.
Handles classical logic.
Majorizability.
Bound extraction.

*Majorizability:*
s* ≥_ρ s ("s* majorizes s of type ρ").
s* bounds functional s.
Uniform bounds.
Higher types.

*Metatheorems:*
If T proves ∀x∃y.A(x,y) with bounds.
Witnessed by functional.
Extractable from proof.
Kohlenbach's metatheorems.

*Applications:*
Fixed point theory: rates of convergence.
Approximation theory: error bounds.
Ergodic theory: quantitative results.
Metric geometry.

*Logical techniques:*
Proof unwinding.
A-translation.
Negative translation.
Bounded collection.

*Results:*
New quantitative theorems.
Sometimes optimal bounds.
Algorithmic content.
Mathematical applications.

**Symbols.**

| Symbol | Unicode | Meaning |
|--------|---------|---------|
| ≥_ρ | — | majorization at type ρ |
| T^ω | — | higher-type extension |
| Φ | U+03A6 | extracted bound |
| ∀∃ | — | prenex form |

**Metatheory.** Bound extraction. Functional interpretation. Metatheorems. Applications.

**Applies to.** Analysis. Fixed point theory. Ergodic theory. Approximation theory.

**Limitations.** Technical prerequisites. Proof complexity. Case-by-case. Limited automation.

© 2026 Lingenic LLC