Sites Inria

Version française

Computer-Assisted Proof

Nathaly Mermet, Technoscope - 6/12/2012

Using the precision of computers to aid mathematics

© Photo Bernard Lachaud

Along with the Typical  research team from Inria Saclay – Ile-de-France, the Marelle  research team from the Inria Sophia Antipolis – Mediterranée research centre has made a major contribution to the Mathematical Components project, led by Georges Gonthier as part of the joint Inria – Microsoft Research laboratory. We take a look back at this exciting experience with Marelle researcher Laurence Rideau

Laurence Rideau, who has been involved in the Mathematical Components project since its inception in 2006, alongside Laurent Théry and Marelle team leader Yves Bertot, explains how the project came into being: "naturally, the project called upon people who had a sufficient knowledge of the Coq tool and were already familiar with mathematical modelling."  The formalisation of mathematics in Coq was at the heart of the project from the start.

"Coq marks a new stage in the computerization of mathematics, with the computer tool not just helping with calculations but actually checking the mathematical reasoning,"  she explains.

Road map

"The goal of the project was very clear,"  says Laurence: it was to develop the tools, the technical and computerized means, to formalise and prove theorems encountered at a Master's level and even in advanced mathematical research.  When it comes to formal proofs, the system does not perform the proof for the researcher, but rather checks that all the steps are coherent and that nothing has been forgotten. "Coq verifies at each step that the building blocks of the theorem are sound and fit together properly," she continues, adding that this tool can be used not only for mathematics but to demonstrate the correctness of procedures or algorithms, including programs.

Concept proving

Initially, the bulk of the work done focused on basic mathematical theories: arithmetic, algebra, and elementary group theory. "But if a mathematical development is well-designed, it can be re-used for other demonstrations,"  suggests Laurence Rideau.

It took four years of work to get to the stage where all the building blocks were in place and the final theorem could be attacked. Proving this theorem then took about another two years. "The day we finished the proof was a great moment for everyone involved,"  she confides, pointing out that she had to painstakingly dissect 600 pages of pure mathematics, and that Georges Gonthier had taken on the hardest parts of the work himself.  The key to this success was excellent teamwork, which allowed progress to be made in mathematical formalisation at every stage of the project. "A computer has limits: it doesn't have mathematical intuition or creativity, so we have to provide it with all the necessary information,"  comments Laurence with a touch of humour. When the proof in Coq is complete, the moment of truth arrives: the computer recalculates everything and displays its verdict! The next step will be to make all these tools available to mathematicians. Watch this space…

Keywords: Mathematical components Project-team MARELLE Coq Inria - Microsoft Research Lab Inria research centre - Sophia Antipolis - Méditerranée