FAQ   Rechercher   Membres   Groupes   S’enregistrer   Profil   Connexion 
Se connecter pour vérifier ses messages privés

Mathématiques

 
Poster un nouveau sujet   Répondre au sujet    la bonne humeur Index du Forum -> Culture Savoir et Art de vivre -> Sciences et technologies
Sujet précédent :: Sujet suivant  
Auteur Message
sami
Invité

Hors ligne




MessagePosté le: Ven 3 Avr - 00:27 (2009)    Sujet du message: Mathématiques Répondre en citant

De nouveaux outils informatiques pourraient révolutionner la pratique des mathématiques en fournissant les démonstrations les plus fiables ayant jamais été produites. Ces outils, basés sur la notion de "preuve formelle", ont été utilisés ces dernières années pour donner des démonstrations presque infaillibles de nombreux résultats importants en mathématiques. Une série de quatre articles écrits par des experts reconnus, et qui vient d’être publiée dans les Notices of the American Mathematical Society, explore des développements nouveaux dans l'utilisation de la preuve formelle en mathématiques.

Lorsque les mathématiciens démontrent des théorèmes de manière traditionnelle, ils présentent leurs arguments sous forme narrative. Ils assument des résultats précédents, ils glissent sur des détails qu'ils pensent que les autres experts comprendront, ils prennent des raccourcis pour rendre la présentation moins pénible, ils font appel à l'intuition, etc. L'exactitude des arguments est déterminée par l'examen minutieux effectué par d'autres mathématiciens, au cours de discussions informelles, lors de conférences, ou dans des articles. Il est important de se rendre compte que les moyens par lesquels les résultats mathématiques sont vérifiés constituent essentiellement un procédé social donc faillible. Quand elle concerne un résultat primordial et bien connu, la démonstration est particulièrement bien contrôlée et des erreurs sont éventuellement trouvées. Cependant l'histoire des mathématiques a connu des résultats faux qui sont restés longtemps non décelés. En outre, pour quelques cas récents, des théorèmes importants exigeaient des démonstrations tellement longues et complexes que très peu de gens ont le temps (Le temps est un concept développé pour représenter la variation du monde : l'Univers n'est jamais figé, les...), l'énergie (Dans le sens commun l'énergie désigne tout ce qui permet d'effectuer un travail, fabriquer de la chaleur, de la...), et le fond de connaissance nécessaire pour en vérifier l’exactitude par eux-mêmes. Enfin, certaines démonstrations contiennent un code informatique (L'informatique désigne l'automatisation du traitement de l'information par un système, concret (machine) ou abstrait....) considérable pour, par exemple, vérifier de nombreux cas qu’il serait impossible de contrôler à la main. Comment les mathématiciens peuvent-ils alors être sûrs que de telles démonstrations soient fiables ?

Pour venir à bout de ces problèmes, des informaticiens et des mathématiciens ont commencé à développer le domaine de la preuve formelle. Une preuve formelle est une démonstration dans laquelle chaque inférence logique est systématiquement contrôlée vis-à-vis des axiomes fondamentaux des mathématiques. Les mathématiciens n'écrivent habituellement pas ces preuves formelles parce qu’elles sont si longues et "encombrantes" qu'il serait impossible de les faire vérifier par des mathématiciens humains. Mais on peut désormais obliger des "assistants informatiques" à procéder à ce contrôle. Ces dernières années, ces assistants sont devenus assez puissants pour manipuler des démonstrations complexes.

Dans quelques cas simples uniquement on peut donner un énoncé à l’ordinateur et s’attendre à ce que celui-ci fournisse une démonstration de lui-même. En règle générale, le mathématicien doit savoir démontrer cet énoncé ; la démonstration est ensuite exposée avec la syntaxe spécifique de la preuve formelle, chaque étape étant définie, et c'est cette preuve formelle que l'ordinateur contrôle. Il est également possible de laisser l’ordinateur explorer des mathématiques qui lui soient propres: il est arrivé dans certains cas que la machine propose des conjectures intéressantes qui étaient passées inaperçues aux mathématiciens. Nous sommes peut-être proches d’un temps où nous verrons les ordinateurs, plutôt que les êtres humains, faire des mathématiques.

Les quatre articles de Notices explorent la situation actuelle de la preuve formelle et fournissent des conseils pratiques pour l’utilisation de ces assistants informatiques. Si l'usage (L’usage est l'action de se servir de quelque chose.) de ces aides se répand, ils pourraient changer profondément les mathématiques telles qu'elles sont actuellement pratiquées. Un rêve à long terme serait de posséder les démonstrations formelles de tous les théorèmes centraux des mathématiques. Thomas Hales, un des auteurs, indique qu'un tel ensemble (En théorie des ensembles, un ensemble, désigne intuitivement une collection d’objets (que l'on appelle éléments...) de démonstrations serait apparentée au "séquencement du génome mathématique (Les mathématiques désignent la science du vrai et du faux en général. C'est-à-dire qu'elle ne s'attache pas à dire ce...)".

Les quatre articles sont:

- Formal Proof, par Thomas Hales, université (Une université est un établissement d'enseignement supérieur dont l'objectif est la production du savoir (recherche),...) de Pittsburgh
- Formal Proof - Theory and Practice, par John Harrison, Intel Corporation (Intel Corporation (mot-valise issu de la contraction de Integrated Electronics) (NASDAQ : INTC) est un centre...)
- Formal proof - The Four Colour Theorem, par Georges Gonthier, Recherche (La recherche scientifique désigne en premier lieu l’ensemble des actions entreprises en vue de produire et de...) Microsoft (Microsoft Corporation (NASDAQ : MSFT) est une multinationale américaine de solutions informatiques, fondée...) , Cambridge, Angleterre
- Formal Proof - Getting Started , par Freek Wiedijk, université de Radboud, Nimègue, Pays (Pays vient du latin pagus qui désignait une subdivision territoriale et tribale d'étendue restreinte (de l'ordre de...) Bas

Ces articles paraissent dans l’édition de décembre 2008 de Notices et sont en consultation libre sur le site de l’AMS.


Revenir en haut
Publicité






MessagePosté le: Ven 3 Avr - 00:27 (2009)    Sujet du message: Publicité

PublicitéSupprimer les publicités ?
Revenir en haut
Montrer les messages depuis:   
Poster un nouveau sujet   Répondre au sujet    la bonne humeur Index du Forum -> Culture Savoir et Art de vivre -> Sciences et technologies Toutes les heures sont au format GMT + 1 Heure
Page 1 sur 1

 
Sauter vers:  

Heures prières


Portail | Index | créer un forum | Forum gratuit d’entraide | Annuaire des forums gratuits | Signaler une violation | Conditions générales d'utilisation
Powered by phpBB © 2001, 2005 phpBB Group
Traduction par : phpBB-fr.com
Theme xand created by spleen.