Une équipe du laboratoire commun Inria – Microsoft Research dirigée par Georges Gonthier a annoncé fin septembre la vérification par un ordinateur, plus précisément par l’assistant de preuve Coq, du théorème de Feit et Thompson, un résultat difficile d’algèbre prouvé en 1963 par deux cent cinquante pages ardues. La nouvelle semble susciter plutôt de la perplexité chez certains mathématiciens : qu’apporte une preuve par ordinateur à un résultat dont personne ne doute ? D’autres collègues, plus enthousiastes, saluent le tour de force de faire vérifier à un ordinateur un des fleurons de la pensée humaine.
ÉCRIT PAR
Jérôme Germoni
Maître de conférences - Institut Camille Jordan, Université Lyon 1
Il est possible d’utiliser des commandes LaTeX pour rédiger des commentaires — mais nous ne recommandons pas d’en abuser ! Les formules mathématiques doivent être composées avec les balises .
Par exemple, on pourra écrire que sont les deux solutions complexes de l’équation .
Si vous souhaitez ajouter une figure ou déposer un fichier ou pour toute autre question, merci de vous adresser au secrétariat.