Vérifier sans faille les démonstrations mathématiques par ordinateur
Publié par Michel le 12/11/2008 à 00:00
Source et illustration: American Mathematical Society
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 (En mathématiques, une démonstration permet d'établir une proposition à partir de propositions initiales, ou précédemment...) est particulièrement bien contrôlée et des erreurs sont éventuellement trouvées. Cependant l'histoire des mathématiques (L’histoire des mathématiques s'étend sur plusieurs millénaires et dans de nombreuses régions du globe allant de la Chine à l'Amérique centrale. Dans la mesure où historiquement la...) 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é par l'être humain pour appréhender le changement dans le monde.), l'énergie (Dans le sens commun l'énergie désigne tout ce qui permet d'effectuer un travail, fabriquer de la chaleur, de la lumière, de produire un mouvement.), 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 - contraction d´information et automatique - est le domaine d'activité scientifique, technique et industriel en rapport avec le traitement automatique de l'information par des machines telles que...) considérable pour, par exemple, vérifier de nombreux cas qu'il serait impossible de contrôler à la main (La main est l’organe préhensile effecteur situé à l’extrémité de l’avant-bras et relié à ce dernier par le poignet. C'est un organe destiné à saisir et...). 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 (La logique (du grec logikê, dérivé de logos (λόγος), terme inventé par Xénocrate signifiant à la fois raison, langage, et raisonnement) est dans une première approche...) 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 (Le mot contrôle peut avoir plusieurs sens. Il peut être employé comme synonyme d'examen, de vérification et de maîtrise.). 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 (Un ordinateur est une machine dotée d'une unité de traitement lui permettant d'exécuter des programmes enregistrés. C'est un ensemble de circuits...) et s'attendre à ce que celui-ci fournisse une démonstration de lui-même. En règle générale, le mathématicien (Un mathématicien est au sens restreint un chercheur en mathématiques, par extension toute personne faisant des mathématiques la base de son activité principale. Ce...) 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 (En géographie, la situation est un concept spatial permettant la localisation relative d'un espace par rapport à son environnement proche ou non. Il inscrit un lieu dans un cadre plus général afin de le...) 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 (AIDES est une association française de lutte contre le VIH/Sida et les Hépatites virales, créée en 1984 et reconnue d'utilité publique depuis 1990. L'association mène des...) 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 (les éléments de l'ensemble), « une multitude qui peut être comprise comme...) de démonstrations serait apparentée au "séquencement du génome (Le génome est l'ensemble du matériel génétique d'un individu ou d'une espèce codé dans son ADN (à l'exception de certains virus dont le génome est porté par des molécules d'ARN). Il...) mathématique (Les mathématiques constituent un domaine de connaissances abstraites construites à l'aide de raisonnements logiques sur des concepts tels que les nombres, les figures, les structures et les...)".

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), sa conservation et sa transmission (études...) 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 de recherche et un industriel américain fabriquant de circuits intégrés...)
- 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 développer les connaissances scientifiques. Par extension...) Microsoft (Microsoft Corporation (NASDAQ : MSFT) est une multinationale américaine de solutions informatiques, fondée par Bill Gates et Paul Allen, dont le revenu annuel a atteint 44,28 milliards de...) , Cambridge, Angleterre (L’Angleterre (England en anglais) est l'une des quatre nations constitutives du Royaume-Uni. Elle est de loin la plus peuplée, avec 50 763 000...)
- 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 quelques centaines de km²),...) Bas

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

Page générée en 0.199 seconde(s) - site hébergé chez Amen
Ce site fait l'objet d'une déclaration à la CNIL sous le numéro de dossier 1037632
Ce site est édité par Techno-Science.net - A propos - Informations légales
Partenaire: HD-Numérique