URL: https://linuxfr.org/users/patrick_g/journaux/voulez-vous-immortaliser-votre-nom Title: Voulez-vous immortaliser votre nom ? Authors: patrick_g Date: 2011年07月20日T01:19:29+02:00 License: CC By-SA Tags: mathématiques Score: 30 Il y a plusieurs solutions envisageables pour immortaliser son nom. Si on est totalement dépourvu de dons et de moyens on peut tenter une stratégie à la [Érostrate](http://fr.wikipedia.org/wiki/%C3%89rostrate). C'est l'approche "je détruis donc je suis". Pas génial mais bon, faute de grives.... Un peu plus subtil est la solution de [Mécène](http://fr.wikipedia.org/wiki/M%C3%A9c%C3%A8ne). Il faut alors avoir énormément d'argent et le dépenser avec générosité pour soutenir les Arts et les Sciences. Ici la difficulté consiste évidemment à rassembler cette immense fortune. Enfin, plus glorieux, on peut essayer d'immortaliser son nom en _créant_ quelque chose, en _produisant_ une œuvre. Qu'il s'agisse d'un roman inoubliable, d'une théorie physique révolutionnaire ou d'un théorème subtil, les créateurs sont assurés de rester dans les mémoires, ou au moins dans les dictionnaires biographiques. Problème : comment parvenir à écrire un roman inoubliable ou à découvrir une théorie physique révolutionnaire ? Ce n'est pas facile ces trucs là ! Peut-être est-il possible de se tourner vers la dernière alternative ? Les mathématiques sont un terrain de jeu infini, donc il devrait être possible de démontrer un théorème quelconque pour lui attacher notre nom et ainsi l'immortaliser...non ? C'est précisément le raisonnement tenu par d'astucieux informaticiens-entrepreneurs de l'Université d'Édimbourg. Ces chercheurs ont créé une compagnie nommée [TheoryMine](http://theorymine.co.uk/) et qui est destinée à vendre des théorèmes originaux à des particuliers en mal d'immortalité. Vous allez sur le site et vous créez un compte. Vous payez 15£ par carte bancaire et hop, deux jours plus tard vous recevez un beau certificat avec votre théorème (comme sur [cette page d'exemple](http://theorymine.co.uk/?go=certificate_example)). Le théorème est **original** et il porte votre nom. ![](http://patrickguignot.free.fr/linuxfr/TheoryMine.jpg) Avouez qu'aux côtés du théorème de Fermat-Wiles ou du théorème de Poincaré-Perelman ça claquerait bien le [lemme](http://fr.wikipedia.org/wiki/Lemme_%28math%C3%A9matiques%29) de pasBill pasGates ou le théorème de baud123 non ? Étant donné qu'un théorème est le résultat de déductions purement logiques, il n'a pas le même statut qu'une simple théorie scientifique réfutable. Un théorème, une fois prouvé, dure pour l'éternité. Et comme ce théorème particulier est nommé d'après vous, alors vous avez _vraiment_ réussi à immortaliser votre nom. CQFD. Comment est-ce que ça marche ? Les chercheurs derrière cette firme travaillent dans le domaine des logiciels [assistants de preuve](http://fr.wikipedia.org/wiki/Assistant_de_preuve), des choses comme [Coq](http://fr.wikipedia.org/wiki/Coq_%28logiciel%29) ou [Isabelle](http://fr.wikipedia.org/wiki/Isabelle_%28logiciel%29). Ici le logiciel se nomme "IsaWannaThm" et il est chargé de générer des théories mathématiques différentes à partir de grammaires qui explorent tout l'espace des fonctions récursives. Cela sonne un peu comme du charabia mais [l'article explicatif au format pdf](http://dream.inf.ed.ac.uk/projects/isaplanner/papers/cacm-theorymine-draft.pdf) est assez clair (voir également [la FAQ](http://theorymine.co.uk/?go=faq)). En gros le logiciel crée des fonctions mathématiques nouvelles à partir d'axiomes de départ à chaque fois un peu différent. Comme ça on est certain que les théorèmes démontrés seront tous originaux et qu'il n'y aura pas de collision avec quelque chose d'existant. Une fois que l'espace de jeu a été défini par "IsaWannaThm" les ordinateurs de l'entreprise TheoryMine utilisent un outil nommé "IsaCosy" pour générer des tonnes de conjectures sur cet espace. Une fois que ces conjectures (des énoncés sans démonstrations) sont listés on peut les faire mouliner par le logiciel "IsaPlanner" qui va utiliser l'assistant de preuve [Isabelle](http://fr.wikipedia.org/wiki/Isabelle_%28logiciel%29) pour les démontrer rigoureusement. [L'article ](http://dream.inf.ed.ac.uk/projects/isaplanner/papers/cacm-theorymine-draft.pdf) précise que les théories récursives sont non décidables en général mais que cela ne pose pas de problème en pratique. Il existe suffisamment de théorèmes démontrables avec un coût computationnel assez réduit pour que la moisson soit riche. Selon les auteurs leur logiciel est capable de générer, avec les seuils de complexité définis actuellement, environ 1016 théorèmes différents. Après l'enchainement "IsaWannaThm" => "IsaCosy" => "IsaPlanner" la boucle est bouclée et, en sortie, nous avons bien un théorème original accompagné par sa démonstration. Si on veut être un peu plus exigeant on pourra se demander si ces théorèmes sont _intéressants_. Après tout les mathématiciens rejettent avec dégoût tout ce qui peut apparaitre comme trivial...alors est-ce que le théorème qui porte votre nom va subir ce triste sort ? La FAQ est assez sibylline à ce sujet :> _TheoryMine applique une série de filtre pour supprimer les théorèmes non intéressants avant de les générer. D'un autre côté ne vous attendez pas à ce que votre théorème vous vaille une [médaille Fields](http://fr.wikipedia.org/wiki/M%C3%A9daille_Fields) !_ Pour avoir plus de détails les lecteurs sont invités à se reporter sur deux articles scientifiques ([1](http://www.springerlink.com/content/bk711q2u247mr967) - [2](http://www.springerlink.com/content/m885557421m7418m)) qui expliquent en quoi les théorèmes sont non triviaux. Si on veut être tatillon on peut quand même considérer que cet achat d'un théorème est une sacrée tricherie et que le détenteur du fameux certificat ne "mérite" pas d'associer son nom à cette démonstration. Après tout il n'a pas fait preuve de créativité ou même de génie pour trouver cette vérité mathématique éternelle. C'est l'ordinateur qui a travaillé et lui s'est piteusement contenté de payer 15£. Pourquoi devrions nous nous souvenir de son nom ? Certes TheoryMine n'est pas une escroquerie, comme peuvent l'être les firmes qui vous vendent des certificats d'étoiles portant votre nom. Là vous avez vraiment un théorème original...mais vous n'avez fait que payer pour l'avoir ! C'est bien sûr une [utilisation très originale](http://www.newscientist.com/article/dn19809-mathematical-immortality-name-that-theorem.html) des travaux sur les démonstrations automatiques et sur les assistants de preuve. Néanmoins je ne suis pas certain que cela remporte un succès extraordinaire auprès du grand public. La notion d'immortalité via les mathématiques est quand même assez abstraite et le fait que la démonstration d'un théorème soit valable éternellement n'impressionne, hélas, pas beaucoup de monde. J'ai bien peur que, pour "immortaliser" leur nom, nos concitoyens ne rêvent plutôt d'être des stars du football.

AltStyle によって変換されたページ (->オリジナル) /