Project Démosthène:
Identity and Geometric Essence of Proofs
ANR Chaire d'Excellence
1.10.2008–30.9.2010


Normalisation on a geometric representation of a proof

1Overview of the Project

The following fundamental question, which we call the `proof identity´ question, is still open:

When are two mathematical proofs the same?

This question has been first formulated by Hilbert, who considered including it in his famous list of open problems. In fact, this problem is often called `Hilbert's 24th problem´. Given the progress we made in the past five years, we expect to find a solution to the proof identity problem in the two years of this project. The tools and techniques that we have to develop will allow a significant advance of the whole field of proof theory, with several applications in computer science.

We need to be able to answer the proof identity question according to several possible criteria by which proofs can be considered the same. This means developing an adequate proof theory, i.e., a formalism in which to express proofs and techniques to manipulate them, called normalisation procedures. The formalism should allow the expression of proofs free of so-called `syntactic bureaucracy´, which arises from the seemingly unavoidable tension between the meaning of a proof and its syntactic formalisation. Proof identity is then defined through normalisation, viz., by transforming a given proof into a standard, bureaucracy-free form, suitable for comparison.

Traditional proof theory does not yield an adequate technology for proof identity, because its formalisms are intrinsically bureaucratic and because it lacks normalisation methods that respect some of the most fundamental properties of proofs, like their size. The purpose of this project is to design the first bureaucracy-free formalism, endowed with an array of novel normalisation notions and techniques, which respect the basic properties of proofs. This will give us the first non-trivial and convincing solution to the proof identity problem.

The main ideas employed in this project are:

  1. proofs are essentially geometric objects;
  2. their geometric shape is their bureaucracy-free essence;
  3. normalisation manipulates the shape of proofs under geometric invariants.

The geometry of proofs is made accessible by a relatively new methodology in proof theory, which Guglielmi pioneered, called `deep inference´. Proofs in deep inference are composed of elementary parts whose size is bounded by a constant. This cannot be achieved in more traditional proof theory, and it is the crucial technical advance that allows us to treat proofs as geometric objects.

Value of this project: 750,448 EUR.

2People

Financed by Démosthène at LORIA–INRIA-Nancy Grand Est:

Main collaborators:

3Related Projects

4Papers

These are the papers that fall in the Démosthène's period (1.10.2008–30.9.2010) and that involve authors financed by the project.

Formalism B is the provisory name of the bureaucracy-free formalism that we propose as a solution to the proof identity problem. Formalism B is based on

  1. the newly acquired knowledge of proof complexity for deep inference (papers with Paola Bruscoli and Michel Parigot),
  2. the experience with the geometric formalism of atomic flows (papers with Tom Gundersen), and
  3. slightly more indirectly, our experience with normalisation in the presence of modalities (papers with Lutz Straßburger).

The formalism is going to be checked for moral and technical compatibility with categorical structures and categorical proof theory, in collaboration with Yves Guiraud and François Lamarche.

5Activity

In the following, AG = Alessio Guglielmi, FL = François Lamarche, LS = Lutz Straßburger, MP = Michel Parigot, NN = Novak Novakovic, PB = Paola Bruscoli, TG = Tom Gundersen, YG = Yves Guiraud. We list here events concerning the project and involving people who are directly financed by Démosthène.


Electric lamps were not invented by improving candles

      30.8.2010Alessio Guglielmiemail