Mon collègue Georges Gonthier, célèbre pour sa preuve formelle du théorème des quatre couleurs, s'est lancé (pas tout seul, heureusement) dans une preuve du théorème de classification des groupes simples finis. Pour le moment, ils en sont à terminer une preuve formelle du théorème de Feit-Thompson. J'ai beaucoup apprécié son exposé à ITP 2011.

Il est bien connu qu'en mathématiques, ce qui compte, ce n'est pas tant de pouvoir fournir des démonstrations aux théorèmes, que de prendre de bonnes définitions pour que les démonstrations ne soient pas trop pénibles (au besoin, on démontrera des équivalences entre définitions). C'est encore plus le cas avec les preuves formelles dans des outils comme Coq, où un mauvais choix de formalisme peut avoir des conséquences catastrophiques sur la faisabilité et la maintenance des preuves. Georges suit en quelque sorte une approche expérimentale : il pose des définitions et regarde à quel point celles-ci « passent bien » sur des théorèmes un tant soit peu non triviaux, afin de se rendre compte d'éventuelles faiblesse avant d'être dans des développements plus importants. Même sur un sujet aussi simple et bien maîtrisé que l'algèbre linéaire en dimension finie ou la définition de ce qu'est un groupe, un choix judicieux de définitions est nécessaire afin d'arriver à prouver des résultats utiles sans peine excessive.