Workshop on Proof Mining 2024

An international workshop on proof mining will be held in Darmstadt, Germany on 4 - 6 of September 2024.
The meeting will take place in person.

The meeting has now concluded. See Participation for a group photo.

With this meeting, we want to initiate a series of workshops dedicated to providing opportunities for people from the diverse areas connected to proof mining to meet, present work in progress and have an interdisciplinary exchange of ideas and knowledge. As such, the topics of interest in particular include logical aspects of proof interpretations as well as applied aspects from in particular nonlinear analysis and optimization.

Proof theory started in the school of David Hilbert in Göttingen in the beginning of the 20th century with what is today known as Hilbert's program, a project in mathematical logic which aimed to show that the use of so-called ideal (i.e. non-constructive, set-theoretic or infinitary) principles in proofs of concrete so-called real statements could be (at least in principle) eliminated. In a modern view, this program is often subsumed under the goal of proving the consistency of powerful theories containing such ideal principles in certain finitistic theories. As is well-known, Gödel's second incompleteness theorem already rules out the provability of the consistency of many theories in themself. 

While Hilbert's program in this specific sense is therefore impossible to achieve globally, Georg Kreisel's work starting in the 1950's under the name of "unwinding proofs" marks the beginning of a seminal paradigm shift in proof theory, namely to use proof-theoretic devices developed in the course of Hilbert's program to extract computational information from specific given mathematical proofs, showing that Hilbert's program is actually largely achievable as far as most proofs from the literature are concerned. This field gained maturity in the 1990's through the work of Ulrich Kohlenbach, since then known as Proof Mining, and by now comprises over 200 works with many case studies situated within numerical mathematics and many branches of modern analysis. 

Current research in this fast-growing area is concerned both with the development of new logical tools designed for facilitating a firm theoretical basis of this enterprise as well as with advancing the range of case studies into new territories relevant also for the mathematicians working in these fields in question.

Scope: 

proof mining in all its facets, in particular comprising the following:

• proof interpretations and, in particular, functional interpretations

• applications to mainstream mathematics in various areas: fixed point theory, monotone operator theory, ergodic theory, number theory, probability theory, etc.

Organizers:

• Ulrich Kohlenbach, Department of Mathematics, TU Darmstadt

• Pedro Pinto, Department of Mathematics, TU Darmstadt

• Nicholas Pischke, Department of Mathematics, TU Darmstadt

Sponsors: