Extracting Quantitative Knowledge from Proofs

The Problem

```

Modern computational methods in engineering, finance, and data science rely on highly complex mathematical models and numerical solvers. Even when convergence or correctness is proven mathematically, these proofs are often qualitative: they guarantee existence or stability but do not provide explicit rates, bounds, or quantitative performance estimates.

This lack of explicit numerical information makes it difficult to assess how theoretical guarantees translate into real-world computational performance.

```

The Logical Approach

```

This project applies tools from Proof Theory and functional interpretations to extract explicit quantitative information from mathematical proofs, a process known as proof mining.

We will:

• Develop and apply new forms of functional interpretations (such as Herbrandized and Uniform Functional Interpretations) to Nonlinear Analysis, Optimization, and Partial Differential Equations.
• Produce computable bounds and convergence rates from non-constructive mathematical proofs.
• Implement prototype tools for semi-automatic proof-theoretic analysis of mathematical results.

The Center for Mathematical Studies (CEMS.UL) is in a unique position to establish a leading research group in Applied Proof Theory and Proof Mining.

The field is currently entering a second wave of expansion, extending beyond classical applications such as Fixed Point Theory, Convex Optimization, and Ergodic Theory into stochastic processes and modern applied mathematics.

```

Industrial Applications

```

• Optimization and Machine Learning: improving algorithms by extracting explicit convergence rates.
• Computational Finance: deriving explicit error bounds in stochastic and numerical methods.
• Engineering Simulation: providing certified guarantees for iterative methods in control systems and mechanics.

```

The Team

```

• Fernando Ferreira (CEMS.UL) – internationally recognized expert in functional interpretations and foundations of mathematics.
• Gilda Ferreira (CEMS.UL) – specialist in proof theory and functional interpretations.
• Pedro Pinto (TU Darmstadt / CEMS.UL) – expert in proof mining and its applications to analysis. Postdoctoral researcher under Ulrich Kohlenbach and recipient of a CEEC grant from Fundação para a Ciência e a Tecnologia.

```

Our Needs

```

• 1 PhD student – development of computational tools for proof interpretation.
• 1 Postdoctoral researcher – advancement of the theoretical framework and application to Optimization, Finance, or Engineering case studies.

This project aims to bridge rigorous logical theory with industrially relevant quantitative information, strengthening CEMS.UL’s position in Applied Proof Theory and Proof Mining.

```