Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

Coq et caracteres images des mathematiques lemonde

Coq et caractères - Images des mathématiques http images math cnrs fr Coq-et-caracteres html Echos de la recherche Coq et caractères Preuve formelle du théorème de Feit et Thompson Jérôme Germoni Une équipe du laboratoire commun Inria Microsoft Research dirigée par Georges Gonthier a annoncé ?n septembre la véri ?cation par un ordinateur plus précisément par l ? assistant de preuve Coq du théorème de Feit et Thompson un résultat di ?cile d ? algèbre prouvé en 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éri ?er à un ordinateur un des eurons de la pensée humaine Lacunes du discours mathématique Malgré tous les e ?orts de son auteur un texte risque d ? être entaché d ? inexactitudes Un exemple tiré de la presse récente L ? Éden mathématique serait par contraste le lieu des vérités éternelles et inattaquables o? de telles imprécisions n ? auraient pas cours Une preuve mathématique devrait partir d ? axiomes si naturels et procéder par étapes si élémentaires qu ? elle doit devenir évidente pour tout autre mathématicien ce qui assure un caractère irréfutable au théorème Beau programme qui trouve son origine dans les Éléments d ? Euclide et précisé vingt-cinq siècles plus tard dans les Principa Mathematica d ? Alfred Whitehead et Bertrand Russell ou les Éléments de mathématique de Nicolas Bourbaki La mathématique formelle ? d ? après Bourbaki Mais si on devait détailler la rédaction à ce point la démonstration du moindre fait signi ?catif deviendrait longue au point d ? en être impossible à lire voire à écrire Aussi les textes mathématiques regorgent de raccourcis qui implicitement signi ?ent il est évident que ? Une preuve est donc écrite pour un public particulier d ? élèves d ? étudiants de chercheurs avec un niveau de détail adapté à ce public ou du moins qui devrait l ? être remplacer npar n n est un problème di ?cile pour un élève de troisième c ? est une évidence pour un mathématicien professionnel Il reste donc au lecteur des étapes à combler La formalisation que Bourbaki a ?rme possible en principe ne semble pas réalisable par un être humain de plus elle obscurcirait plutôt les choses et on n ? aurait rien à y gagner of Un théorème des Principia Mathematica de Whitehead et Russell et une preuve sans mots thèse et antithèse CCoq et caractères - Images des mathématiques http images math cnrs fr Coq-et-caracteres html Un théorème des Principia Mathematica de Whitehead et Russell et une preuve sans mots thèse et antithèse En général combler les étapes manquantes du discours mathématique se fait sans mal Sinon modulo les convenances sociales le lecteur élève mathématicien relecteur d ? une revue est en droit de demander des éclaircissements à l ? auteur professeur chercheur Mais