Mathematical proof by computer science!
© Photo Bernard Lachaud
A complete formal proof, certified by the Coq software, was announced in September by Georges Gonthier and his team at the Inria-Microsoft Research joint laboratory.
This work renders the conflict between computer science and mathematics obsolete, the common denominator being logic. Two young researchers who joined Georges Gonthier for the ride told us how much they enjoyed participating in the work and "grew" as a result of the Mathematical Components (MathComp) project. Here's what they had to say...
Do you feel privileged to have contributed to the success of Georges Gonthier's latest work?
© Inria / Photo Kaksonen
Assia Mahboubi, research agent at Inria since 2007 and MatchComp team member since 2006.
Georges Gonthier already had a big reputation before the success of this project on a formal proof of the Feit-Thompson theorem. He's made many contributions to computer science, but his verification of the four colour theorem, in collaboration with Benjamin Werner (Inria), brought a lot of attention to our project.
© Photo Bernard Lachaud
Enrico Tassi, research agent at Inria since September 2012 following post-doctoral studies on the project (completed at the end of 2011). He worked on the project as part of his thesis in Bologna (Italy) for six months (end of 2006/beginning of 2007).
I really liked the idea of doing maths with a computer and having verification of a proof as the goal. Studying and developing tools like Coq was the central theme of my master's and thesis studies. The Inria-Microsoft Research joint laboratory had just been set up and it was an excellent opportunity to come to work with the field's top experts.
What does this field of research represent for you and what's the basis for your motivation?
Assia Mahboubi : It was a fairly cross-disciplined activity that also questions the philosophical notion of mathematical truth, even though it can provide answers to the modern needs of computer security. It's extremely difficult to be absolutely confident in the proof of a theorem. We try to transcribe the mathematical statements and their proof in the very simple and perfectly coded language that is logic so that a computer can help us to verify them. There are multiple aspects to this research, and it poses a number of questions: what is a mathematical proof? What is a programme? What is logic?
Enrico Tassi : When is an argument valid? This problem has been studied for hundreds of years, by philosophers such as Aristotle to mathematicians such as Hilbert and Gödel. Our research attempts to positively answer the following questions: can computers help man to formulate complex and original arguments without causing error? Can they help scientists faced with the growing complexity of the mathematical theories that they're developing?
How do you see the future in the light of this now completed project?
Assia Mahboubi : The idea of using a computer's help to create proofs is nothing new: it's been an area of research at Inria for several decades. What's new about this achievement is that the approach has come into its own for "major proofs" and "major theorems". Numerous fields using critical computer programmes (aeronautics, cryptography, etc.) are already benefiting from the applications of this field of research. However, we now think that it might also be of interest to a wider range of scientists, including mathematicians who have until now only used paper and blackboards.
Enrico Tassi : The finished project shows that it's possible to verify complex mathematical theorems using a computer. However, the work isn't over, as this technology still needs to be made usable by all scientists and not just by formal proof experts such as ourselves.
These articles could interest you:
- © Inria / Photo Kaksonen Computer-assisted proof A major success for computer-assisted proof
- © Laboratoire commun Inria-Microsoft Research Computer-assisted proof "Our work diagram looked like a Napoleonic war plan!"
- © Photo Bernard Lachaud Computer-Assisted Proof Using the precision of computers to aid mathematics