Material Interpretation

Mathematical proofs explain why certain statements are true and others are not. However, these explanations often remain very theoretical. The "Material Interpretation" project aims to turn these theoretical proofs into practical tools that can solve concrete problems. The main goal is to extract algorithms from mathematical proofs. For example, given a proof of the statement "For all x, there exists a y with property P.", we want to obtain not just an abstract statement of existence, but actually a function f that constructs a specific y = f(x) with property P for each x. In this way, abstract mathematical proofs are brought to life and find practical applications. To achieve this, we use so-called proof assistants. These are programs that help to create, store and work with formal proofs on a computer. In particular, one can apply proof interpretations to these formal proofs. Proof interpretations are algorithms that are applied to proofs, either to obtain functions, such as the function f described above, or to obtain other proofs, for example for more general or more constructive theorems. An important part of the project will be to develop a new proof interpretation: The material interpretation should stay as close to the original proof as possible, while providing more constructive content. For example, a proof of the statement "A implies B" should ideally be transformed into a statement of the form "not A or B". This latter statement is constructively stronger, since at least one must decide whether "not A" is true or "B" is true. The aim is to make the material interpretation accessible to as large a class of statements and proofs as possible. This class will include proofs whose material interpretation solves open problems, such as a new constructive variant of Hilbert`s 17th problem. To achieve the goals of the project, we will make use of the specialisations and advantages of different proof assistants. We will compare the advantages and disadvantages of proof assistants and use the most useful one. Additionally, an appropriate overview will contribute to expand individual proof assistants and improving their cooperation.