Vérifier sans faille les démonstrations mathématiques par ordinateur

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, l'énergie, 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 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 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 de démonstrations serait apparentée au "séquencement du génome mathématique".

Les quatre articles sont:

- Formal Proof, par Thomas Hales, université de Pittsburgh

- Formal Proof - Theory and Practice, par John Harrison, Intel Corporation

- Formal proof - The Four Colour Theorem, par Georges Gonthier, Recherche Microsoft , Cambridge, Angleterre

- Formal Proof - Getting Started , par Freek Wiedijk, université de Radboud, Nimègue, Pays Bas

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