Team Meeting: Faustine Oliva

Faustine Oliva is a doctoral student at Université d’Aix-Marseille. Her project is about the significance of computer-assisted proofs for mathematical knowledge.

In what sense are (computer-assisted) proofs experiments?

The Four Color Theorem (4CT) states that four color suffice to color any planar map in such a way that no two adjacent regions have the same color. As its proof (Appel & Haken, 1977, 1977) involves a large number of computations, it is based on the output of a computer program. Tymoczko in (Tymoczko, 1979) argues that the controlled use of a computer program corresponds to the implementation of a computer expriment. It is therefore a proof, part of which consists of an experiment. In 2005 the formalization of the 4CT proof in a programming language within the environment of the proof assistant Coq (Gonthier, 2005) was completed. In such software a proof is also a computer program: the proof assistant checks the validity of the former by certifying the correction of the latter in relation to its specification. This proof no longer integrates a computer program, it becomes a computer program. In what sense can we say that this formalized proof is an experiment? To answer this question we briefly outline Tymoczko’s analogy between mathematics and the empirical sciences and specify the characteristics of what he calls a “computer experiment”. We then detail the steps involved in formalizing and checking the 4CT proof in Coq before discussing how this formalized proof can be viewed as an experiment and relating this approach to other conceptions of mathematical proof as experiment.

Faustine is a doctoral student at Université d’Aix-Marseille.