| Résume | Les assistants de preuve sont des logiciels qui permettent de formaliser, manipuler, vérifier des énoncés mathématiques et leurs preuves dans un langage logique parfaitement codifié. L'un des bénéfice ---mais pas le seul--- de ce travail de formalisation est qu'il rend complètement mécanique le processus de vérification des démonstrations. Ce exposé est consacré à la formalisation achevée en 2012 d'une démonstration du théorème de l'Ordre Impair (W. Feit, J. G. Thompson, 1963) à l'aide de l'un de ces assistants de preuve, le système Coq. Nous discuterons les différentes natures d'ingrédients mis en oeuvre dans un tel travail, à l'intersection entre mathématiques et informatique. |
