Mathematical Conversations

Black (or white) board is probably one of the most precious companions to many mathematicians. However, computers now also play an increasing role in the everyday activity of a researcher in mathematics: for typesetting articles, for testing conjectures, and sometimes even for validating parts of proofs by large computations. A maybe less known family of software, called proof assistants, also aim at ``doing mathematics with a computer". These systems allow their users to check with the highest degree of certainty the validity of the proofs they have carefully described to the machine. A first landmark was obtained in 2005 with the complete verification by such a proof assistant of the controversial proof of the Four Colour Theorem, which combines combinatorial reasoning with large scale computations beyond the reach of pen and paper calculations. Last September a proof of the Odd Order Theorem (Feit-Thompson, 1963), which is a milestone for the Enormous Theorem of the classification of finite simple groups, has also been verified by the Coq proof assistant. This time, the computer is used to check a proof which does not rely on heavy computations but on a sophisticated combination of mathematical theories resulting in the longest published proof at its time. We will see how this last achievement illustrates the quite wide variety of research areas and methodologies that should combine in order to ensure the success of such a project. Black (or white) board will eventually never be surpassed to convey and give rise to the intuitions of the mind who discovers new mathematics, but having proofs checked by a machine rather by a human reviewer may open some new perspectives we will hopefully discuss.