Les mathématiques se construisent avec deux modes de raisonnement dissemblables: un coté "soft" abordant les idées et les analogies et un coté "hard", concernant les vérifications. Le coté "hard" est le plus facile à cerner. Il concerne en premier lieu, les preuves "formelles", composée chacunes d'une série d'assertions. Un mathématicien peut vérifier si la démonstration est correcte en la parcourant, pas à pas, et en testant si chacune des étapes suit la précédente à partir de faits déjà démontrés de façon correcte.
Le coté "soft" est le moins facile à décrire. Il est formé d'intuitions sur les objets formels construits dans les démonstrations mathématiques; d'idées qu'une partie des mathématiques peut correspondre de façon analogique à une autre partie des mathématiques; ou aussi d'analogies entre les objets mathématiques et le monde physique.
Par exemple, si vous voulez montrer que deux objets sont similaires, il est parfois plus facile de montrer indirectement qu'ils le sont tous deux à un troisième.
Le langage que les mathématiciens utilisent dans les livres et les articles comble le fossé entre ces deux modes de raisonnement. Il est difficile, pointilleux et présente des démonstrations rigoureuses; mais il tente aussi de transmettre subtilement, d'éphémères et intangibles idées "soft" à l'intérieur de sa constitution "hard", au travers d'analogies, d'allusions et d'autres moyens indirects. Ces idées "soft" sont rarement exposées en quelques mots; on ne trouve que très rarement une phrase qui peut résumer à elle seule toutes les idées contenues dans une preuve. Mais un texte mathématique technique et précis peut construire lentement une toile d'éphémères et intangibles concepts par un choix pertinent de mots, traçant des parallèles entre les différentes parties de mathématiques et des sens similaires. Ainsi, un homme mathématicien peut-il se laisser conduire par le texte jusqu'aux idées sous-jacentes. Et, in fine, ce sont ces idées "soft" qui constituent la matière. Le contenu "hard" est important car il rend objectif et vérifiable, mais ce sont les idées "soft" qui sont le centre des mathématiques, ce que les mathématiciens recherchent
En raison de cette nature duale, le langage des mathématiques présente une remarquable opportunité pour les ordinateurs. Les ordinateurs sont très forts du coté "hard" mais très mauvais du coté "soft". Le langage des publications mathématiques, qui capture le "soft" au milieu du "hard", nous donne une opportunité unique de permettre aux ordinateurs d'approcher le raisonnement "soft". Malheureusement, l'approche actuelle des ordinateurs vers les mathématiques, est celle de programmer des programmes de preuve de théorèmes, ne faisant rien d'autre que ça. Du point de vue des mathématiciens, de tels programmes ont trois déficiences. Premièrement, l'interaction avec eux implique l'utilisation de langages impénétrables, très éloignés du langage normal des mathématiques. Deuxièmement, les ordinateurs sont très mauvais en mathématiques - ils ne peuvent pas vérifier tous les sous-niveaux de preuve sans une assistance humaine. Troisièmement, ils ont seulement la capacité de faire des mathématiques "hard"; dans de très rares cas où ils prouvent de nouveaux résultats, ils les ont prouvés en n'ajoutant aucune idée nouvelle. Ce type de preuve n'intéresse guère les mathématiciens.
Ces trois déficiences sont en fait liées. Les programmes de preuve de théorème sont inefficaces en mathématiques précisément parce qu'ils ne sont pas en mesure de contenir d'idées "soft". Et les idées "soft" ne sont pas explicitement dites, mais implicitement absorbées dans le langage usuel des mathématiciens utilisé quotidiennement. Les humains semblent dans l'incapacité d'extraire de telles idées à partir langages exotiques et appauvris utilisés dans les programmes de preuves courants - mais ce n'est pas une raison pour penser que les ordinateurs sont dans l'incapacité de le faire. L'actuel langage "hard" nous donne une prise très imparfaite sur les idées "soft" sous-jacentes; mais c'est encore la meilleure prise que nous ayons.
Pour les raisons qui viennent d'être expliquées, ces trois premiers objectifs de la thèse de Mohan Ganesalingam (dont c'est l'introduction) sont: de construire un langage informatique qui est très proche du langage réel des mathématiques, d'écrire le corps des mathématiques dans ce langage en y incluant les idées "soft" pour un mathématicien humain, et permettant à l'ordinateur d'extraire quelques unes de ces idées - même si ce n'est pas aussi bien qu'un humain, l'ordinateur pourra quand même vérifier des preuves écrites en langage mathématique normal.
La difficulté n'est pas tellement celle liée aux ordinateurs. Écrire des programmes est plutôt facile, mais savoir ce qu'ils doivent faire est difficile. Avant de construire un langage informatique ressemblant au langage réel des mathématiciens, il est nécessaire de le comprendre extrêmement bien; il n'est pas suffisant d'en avoir une simple idée intuitive, un sentiment subjectif du langage mathématique que les mathématiciens ont, mais une analyse formelle, objective et précise en tout point.
Lorsque l'on fait des recherches pour une telle analyse, la science informatique existante et les analyses de langages informatiques ne sont guère utiles; l'intégralité des langages construits par l'homme analysés par les ordinateurs sont extrêmement simples comparés aux mathématiques qui ont été développées au travers des siècles; notre meilleur espoir est de se tourner vers les linguistiques modernes qui visent à mettre à nu les riches structures des langages humains complexes. Les mathématiques diffèrent suffisamment des langages humains pour que très peu de linguistique théorique puisse être directement utilisée; la majorité des matériaux doit être reconstruite. Mais les linguistiques, donnent au moins, le cadre général d'une analyse formelle d'un langage; cela donne l'état d'esprit et le point de départ.
On présente souvent les mathématiques comme étant abstraites et incompréhensibles avec une structure chaotique:
Heureusement la réalité est vraiment différente. Les mathématiques sont écrites avec des phrases et des paragraphes, comme le langage écrit en général. Les phrases contiennent un mélange de mots et de symboles mathématiques. Pour comprendre le langage mathématique, il est nécessaire de comprendre quelle est la fonction des mots, quelle est celle des symboles et comment ajuster les deux.
Le travail est difficile car les mots et les symboles doivent avoir un seul sens déterminé. Or un mot comme "premier" peut avoir une douzaine de sens et une simple expression du type "x+y" aussi en fonction du contexte. En d'autres termes, l'ambigüité est un problème. Il est nécessaire d'avoir une théorie qui élimine toutes ces ambigüités et qui permet de prédire quel sens est à privilégier dans un contexte donné. Il n'existe cependant aucune technique linguistique permettant d'éliminer toutes les ambigüités en mathématiques. Les nombres se comportent parfois comme s'ils n'en étaient pas, parfois comme s'ils en étaient et des objets qui ne le sont pas se comportent parfois aussi comme s'ils en étaient! Ainsi la notion de type n'est pas pertinente. Il faut clarifier cette notion de type qui se trouve enchevêtrée en mathématiques.
J'arrête ici de poursuivre la traduction de l'introduction de la thèse à la jointure de l'informatique, de la linguistique et des mathématiques. J'ai pris beaucoup de plaisir à faire cette traduction sur un sujet émergeant. J'espère qu'il en aura été de même pour vous. J'espère aussi ne pas avoir commis trop de contresens mais comme à l'accoutumée, les liens vers le texte original sont disponibles et permettent de s'y référer. Je n'ai pas poursuivi plus avant la lecture de la thèse car mon faible niveau de mathématique et la fastidieuse lecture de l'anglais qui lui est adjoint ne me permettent guère de le faire.
Quelques liens intéressants: