En informatique ou en mathématiques assistées par informatique, un assistant de preuve est un logiciel permettant l'écriture et la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques, soit sur des assertions relatives à l'exécution de programmes informatiques. Il existe différents logiciels permettant de vérifier des preuves mathématiques et informatiques : Coq, Isabelle, Mizar, PhoX, PVS. Cependant nous nous concentrerons ici sur le logiciel Coq, car c'est celui utilisé par Georges Gonthier pour vérifier la preuve de 1995. Chaque logiciel se base sur un langage de programmation particulier. Pour le logiciel Coq, il s'agit du langage Gallina.

Coq, comme son nom l'indique, est un assistant de preuve français. En réalité, il s'agit de l'acronyme de Calculus of Constructions, et d'un jeu de mot vis-à-vis de l'inventeur du calcul de constructions, Thierry Coquand. Coq est fondé sur la théorie des types et non sur la logique axiomatique classique, ce qui signifie qu'il est nécessaire de redémontrer des propositions triviales ou très simples avant de pouvoir espérer prouver ce qui nous intéresse. L'avantage est que le script de preuve final est solide formellement, car il ne dépend pas d'axiomes qui pourraient être mal interprétés par le logiciel. Il est intéressant de remarquer que la logique à l'œuvre au sein de Coq emprunte à deux théories concurrentes du début du XX^ème siècle : la calculabilité et la constructivité. La première correspond à la théorie des types développée par Alonzo Church à la suite de Russell et Whitehead, et repose sur le concept de lambda-calcul. La seconde est incarnée par la théorie des types intuitionniste de Per Martin-Löf, et se fonde sur la construction de témoins.

Pourquoi les assistants de preuve ont-ils été créés ?

Le premier projet d'assistant de preuve date de 1967. C'est le projet Automath du mathématicien néerlandais Nicolaas Govert de Bruijn dont le but était de formaliser des théories mathématiques complètes dans un langage informatique de manière à inclure un assistant de preuve qui pouvait en vérifier la correction. Si le système Automath apportait de nombreuses notions novatrices qui ont été adoptées ou réinventées ultérieurement, il faut cependant attendre les années 1990-2000 pour que les assistants de preuve commencent à se développer. On peut déterminer trois grands facteurs explicatifs du développement des assistants de preuve.

• Le facteur économique
  Le développement fulgurant de l'informatique et de la micro informatique dans les années 1990 a nécessité de nouveaux logiciels pour prouver que les systèmes d'exploitations produit par des entreprises comme Microsoft ne présentaient pas de bug. Il est ainsi à noter que Georges Gonthier a longtemps travaillé grâce aux financements de l'entreprise Microsoft.

• L'enjeu du développement des assistants de preuve face aux limites du peer reviewing
  Le développement des preuves formelles est en partie lié aux limites du peer reviewing traditionnel. Ce système est basé sur le contrôle de la communauté scientifique, qui vérifie les preuves soumises par des confrères. Cependant, cela ne garantit pas la correction systématique des erreurs. En effet, Assia Mahboubi nous a ainsi rappelé en entretien que dans les domaines de mathématiques "pures", sans calculs spécifiques à vérifier, le niveau de technicité était tel qu'une minorité de mathématiciens seulement était susceptible de pouvoir vérifier une preuve. Peu de personnes sont en réalité en mesure de faire la relecture des preuves publiées. D'après Assia Mahboubi, la réputation de l'auteur est un facteur important de la validation de la preuve, plus que la relecture. Il est ainsi très courant que des "papiers faux" soient publiés dans les revues scientifiques spécialisées. Les limites du peer reviewing sont ainsi une des raisons principales du développement des assistants de preuve tels que Coq, qui peuvent permettre de systématiser la vérification et de limiter le nombre d'erreurs. Par ailleurs, l'utilisation d'assistants de preuve pourrait décharger les mathématiciens d'une partie de la relecture des articles de leurs collègues, travail souvent jugé chronophage vis-à-vis de leur recherches personnelles. "Il y a très peu de gens qui sont en mesure de faire une relecture experte de certains sujets et puis il y a la réputation de l'auteur qui joue. Enfin ce sont tout un tas de facteurs qui font qu'il y a plein de papiers faux." (Assia Mahboubi)

• L'assistant de preuve comme solution face à la multiplication des preuves géantes
  La nécessité des assistants de preuve s'est enfin fait sentir avec la multiplication des preuves dites "géantes" dépassant la centaine de pages et ne pouvant être que difficilement relues par une seule personne. On pourra citer de manière non exhaustive la preuve du théorème de Feit-Thompson rédigée en 1963 , la preuve de la conjecture de Kepler rédigée en 1998, faisant plus de 300 pages chacunes, ou encore la preuve du dernier théorème de Fermat publiée par Andrew J. Wiles en 1993.

Le travail effectué de Georges Gonthier et de son équipe a été de transcrire la preuve du théorème des quatre couleurs de 1995 dans le langage Gallina, pour être vérifiée par le logiciel Coq. Cette tâche qui peut paraître simple au premier abord a demandé plusieurs mois de travail à Georges Gonthier et à toute son équipe.

Retour sur la preuve de 1995

La preuve produite par Robertson, Saunders, Seymour et Thomas en 1995 se décompose en deux parties. La première partie consiste en un article de 35 pages démontrant que la démonstration du théorème revient à analyser 633 configurations et à effectuer 1 000 000 000 de coloriages différents sur 10 000 cartes. La seconde est un programme écrit en langage C traitant les différents cas énoncés plus haut. Le problème était de s'assurer que le programme écrit en C corresponde bien à la description mathématique énoncée dans l'article et que le contenu même de l'article soit juste.

Le travail de Georges Gonthier

La difficulté du travail de Georges Gonthier n'est pas en réalité d'avoir transcrit le programme de preuve écrit en langage C en programme Coq, travail qui n'a pris que quelque mois, mais de formaliser un script de preuve Coq pour l'article de 35 pages. En effet tout article de mathématiques mobilise des savoirs tacites acquis par ceux qui les lisent lors de leurs années d'études. Le travail de l'équipe de Georges Gonthier a donc été de trouver une formalisation rigoureuse des définitions des concepts les plus simples, dont la transcription en script Coq nécessite cependant une recherche mathématique intense. Cette formalisation s'attaque à des résultats aussi simple que l'affirmation 1 + 1 = 2.

La conséquence de ce travail est la certification de la justesse des liens logiques entre les arguments de la partie manuscrite de la preuve et l'assurance de l'absence de bugs dans le code en C. Pour plus d'informations sur le travail de Georges Gonthier et de son équipe nous vous invitons à regarder un extrait d'une de ses conférences au sujet de sa vérification de la preuve du 4CT. (du début jusqu'à 18:50)

En 1976, la controverse autour de la preuve de Haken et Appel se structurait autour de deux problèmes. L'un était formel et portait sur la présence ou non d'erreurs dans la partie manuscrite et de "bugs" dans la partie informatique. L'autre était informel et s'articulait autour de la nature même d'une preuve mathématique. Le travail de l'équipe de Georges Gonthier rend peu à peu le premier problème en partie obsolète.

Par ailleurs, les progrès de l'informatique depuis les années 1970 limitent les risques de bugs, et les programmes sont beaucoup plus sûrs désormais qu'ils ne l'étaient auparavant. En ce qui concerne Coq, le noyau du logiciel est extrêmement simple, à un tel point que Pierre-Evariste Dagand a pu nous en détailler le fonctionnement en une vingtaine de minutes au tableau ! Comme nous l'avons dit, Coq repose sur le calcul des constructions : il "suffit" donc de définir en logique intuitionniste les quantificateurs "il existe" (∃) et "pour tout" (∀) ainsi que l'égalité, et le tour est joué. "Coq ne fait rien seul," nous rappelle Pierre-Evariste Dagand, "cette construction-là est complètement décidable, complètement mécanique, il n'y a pas de travail d'invention : Coq ne fait que vérifier des choses". En se fondant sur ce noyau, il est alors possible de démontrer formellement des propositions de plus en plus complexes, chaque lemme démontré devenant alors une hypothèse servant à démontrer la suite. De plus, comme Coq ne repose sur aucun axiome à la base, il offre une très grande flexibilité quant au cadre théorique dans lequel on souhaite faire sa démonstration, comme nous l'explique Théo Zimmermann : "Ce que ça signifie, ces histoires d'axiomes qu'on choisit de ne pas inclure par défaut, ça signifie qu'il n'y a pas qu'une vérité absolue. On peut démontrer des théorèmes en se basant sur un certain nombre d'axiomes, mais si on part d'autres axiomes, d'autres postulats, on peut démontrer d'autres théorèmes éventuellement incompatibles."

Ainsi, pour Robert Pollack , l'émergence des assistants de preuve décale le problème de la confiance dans la preuve. Il ne s'agit plus de comprendre et de croire dans la preuve papier et dans les liens logiques qu'elle décrit, mais de comprendre comment fonctionne le noyau de l'assistant de preuve. En cela, accepter une preuve serait réductible à la question de la confiance dans l'assistant de preuve, et à la question de la réplicabilité de la vérification de la preuve par plusieurs mathématiciens. Le débat autour du théorème se recentre alors autour de la définition de la nature d'une preuve mathématique. La question est ici de savoir si l'arrivée de l'informatique révolutionne véritablement la manière de faire et de définir une preuve mathématique.

L'importance de la notion de consensus

La preuve de 2004 par Georges Gonthier semble clôturer la controverse quant à l'acceptation d'une preuve informatisée du 4CT, non seulement car elle met fin aux problèmes techniques présents jusqu'alors, mais également parce qu'elle est consensuellement acceptée par la communauté mathématique. Cette notion éminnement sociale de consensus est centrale et primordiale dans l'acceptation d'une preuve. David Aubin l'évoque très clairement lors de notre entretien : "Ce qui est important dans une preuve mathématique, ce n'est pas nécessairement qu'elle soit absolument certaine, mais bien qu'elle soit acceptée par une communauté". De même, Jean-Jacques Szczeciniarz insiste sur ce point : "Pour les mathématiciens, est essentielle la question de la forme d'adhésion, de la conviction que la preuve l'emporte, et c'est toute la communauté qui se met d'accord." Une preuve ne tient donc pas uniquement à un aspect purement mathématique et théorique. Pour certains philosophes des mathématiques, la preuve est même indissociable de cette étape du consensus. Nicolas Balacheff, chercheur en informatique, donne ainsi dans "Processus de preuve et situations de validation" la définition suivante de la preuve: "Nous appelons preuve une explication acceptée par une communauté donnée à un moment donné". De même, Yuri Manin, mathématicien renommé, affirme en 1977 qu'un argument devient une preuve après l'acte social de l'accepter en tant que preuve.

De fait, si la preuve de 1976 d'Appel, Haken et Koch est restée controversée, c'est parce qu'elle ne fait pas l'adhésion de la communauté mathématique, tandis que la preuve de Georges Gonthier a fait consensus et a été globalement acceptée par la communauté. Ainsi, cette preuve de Georges Gonthier peut marquer la clôture de la controverse autour des preuves du 4CT justement parce qu'elle est considérée comme juste et correcte par une majorité de la communauté mathématique. Par ailleurs, la majorité des personnes que nous avons interrogées ont précisé qu'elles ne considéraient pas qu'il y ait encore une controverse aujourd'hui (voire doutent que cette controverse ait jamais existé). David Aubin affirme par exemple : "A mon sens, il n'y a pas une énorme controverse sur la preuve du 4CT". La controverse de ce point de vue semble donc fermée, et notamment parce qu'il y a consensus sur la preuve de Gonthier.

Cependant, la notion de consensus elle-même a des implications qui amènent à réfléchir sur la fermeture de la controverse autour des preuves du 4CT. En effet, étant donné qu'une preuve a besoin d'être acceptée pour être considérée comme telle, elle doit avant tout être comprise. Comme l'explique Théo Zimmermann : "Une preuve est avant tout un objet de communication. Il faut pouvoir convaincre son assistance que le théorème est correct. Cela tient plus au langage et à la communication avec les autres". Jean-Jacques Szczeciniarz insiste également sur ce point : "Une fois qu'une preuve a été trouvée, il y a un re-travail qui se fait sur la preuve et qui peut durer assez longtemps, pour la simplifier un maximum afin qu'elle puisse être comprise et transmise par et auprès de non-spécialistes". Ainsi comme le suggère Szczeciniarz, la question du consensus autour de l'acceptation d'une preuve est liée à l'accessibilité et à l'intelligibilité de ladite preuve. A titre d'exemple sur cette question, Zimmermann évoque le mathématicien Shinichi Mochizuki, qui, après des mois de travail solitaire, publie une preuve de la conjecture ABC (un célèbre problème en arithmétique) sur près de 500 pages. Cependant sa preuve est extrêmement compliquée, et utilise un langage et des outils que lui-même a créés et qu'il refuse d'expliquer plus en avant. Alors que de nombreux mathématiciens essaient de reprendre et de comprendre cette preuve, se pose la question de savoir si cette preuve en est bien une, car s'il n'y a pas de consensus, peut-il y avoir une preuve ? Cet exemple montre l'importance de thèmes comme l'élégance, le langage ou l'accessibilité d'une preuve.

De fait, bien que la controverse sur les preuves du 4CT semble avoir été fermée par la preuve de Gonthier, celle-ci fait actuellement l'objet d'un travail de simplification, notamment en ce qui concerne Coq. Cela nous amène à nous interroger sur la fermeture de cette controverse. Ainsi, pour Assia Mahboubi, la controverse n'est pas encore fermée car il reste encore, entres autres, le problème de l'accessibilité de Coq, qui rend la preuve de Gonthier encore illisible pour bon nombre de personnes incompétentes sur l'utilisation de Coq. Il est alors intéressant de se questionner non plus sur la fermeture de la controverse étudiée jusque-là mais plutôt sur sa mutation.

Lors de nos entretiens, une caractéristique fondamentale de l'acceptation d'une preuve a été énoncée par plusieurs de nos interlocuteurs. C'est celle du caractère explicatif de la preuve. Au delà de la validation d'un théorème, une preuve mathématique doit en effet apporter des informations supplémentaires permettant une meilleur compréhension des objets mathématiques mobilisés dans le théorème.

Un problème se pose avec des preuves sous forme de grande disjonction de cas traités informatiquement puis vérifiés par un assistant de preuve. En effet, la taille de la preuve et de sa vérification sont telles que le lecteur mathématicien lambda ne peut considérer que le résultat booléen donné par l'ordinateur : soit la preuve est vraie, soit la preuve est fausse. Selon Pierre-Evariste Dagand : "Gonthier a pris des preuves qui étaient énormes, et ils les a vérifiées par ordinateur ; mais à la fin, il n'a pas trouvé que la preuve était fausse, donc est-ce qu'on a gagné quelque chose ? Je ne sais pas."

Georges Gonthier se défend de cette affirmation. Selon lui, le travail de redéfinition rigoureuse de concepts mathématiques en langage Gallina apporte de nouvelles connaissances mathématiques sur les objets mobilisés dans la preuve. Un exemple simple de l'apport de la formalisation dans la compréhension des objets mathématique est la définition formelle d'une carte. En effet, tout le monde sait à quoi ressemble visuellement l'affirmation "on colorie une carte, et pourtant il semble difficile de définir mathématiquement la notion de carte. Dans la preuve de 1995, la notion de carte est réduite à celle de graphe. Cependant la notion de graphe ne remplit pas les conditions nécessaire pour décrire une carte planaire. La preuve de 1995 mêle donc des notions de mathématiques combinatoires et de topologie pour parvenir à la démonstration, ce qui est impossible à exprimer formellement par ordinateur. Un des apports de Georges Gonthier est donc d'avoir défini rigoureusement le concept de carte. Cependant l'accessibilité à ces définitions et au travail fourni par Georges Gonthier reste en partie conditionnée au problème de la maîtrise du logiciel Coq.

Le domaine des assistants de preuve voit le développement d'une nouvelle branche de recherche. De plus en plus de scientifiques travaillent sur les moyens dont les assistants de preuve tels que Coq peuvent être rendus plus accessibles. En effet, si Gonthier a permis de créer un consensus sur la preuve de 1995 du théorème des quatre couleurs, il a aussi ouvert le champ d'application de Coq. La vérification de la preuve de 1995 par Coq n'est qu'une étape du développement potentiel des applications possibles des assistants de preuve. Cependant, l'obstacle principal à ce développement est le problème de l'accessibilité du langage et du fonctionnement des assistants de preuve. La plupart des mathématiciens ne sont pour l'instant pas en mesure d'utiliser des assistants tels que Coq pour la vérification de preuve.

Les enjeux de l'accessibilité des assistants de preuve

Si le sujet principal de préoccupation réside dans la possibilité d'erreurs dans les publications scientifiques, le problème est différent pour la vérification formelle par les assistants. Quand Coq vérifie une preuve informatique, le rapport final donné par l'assistant de preuve n'est pas rédigé de manière compréhensible pour un mathématicien. C'est pour cette raison que des travaux sont menés pour rendre Coq plus accessible et intelligible.

Théo Zimmermann, avec lequel nous nous sommes entretenus, travaille justement sur ces problématiques. Selon lui, l'enjeu est de rendre le rapport final produit et les "scripts de preuve" par Coq vérifiables par un mathématicien sans avoir à utiliser Coq. Il explique ainsi qu'actuellement, le travail sur l'accessibilité des assistants de preuve n'est pas à un stade assez avancé pour que des personnes non expertes puissent vérifier une preuve. L'enchaînement de blocs de bases que constitue le script final de Coq devrait pouvoir être traduit en un langage similaire à celui des revues scientifiques.

Le problème du langage se pose aussi lorsque des preuves "traditionnelles" sont vérifiées par les assistants de preuve. Assia Mahboubi indique ainsi que les publications concernant les preuves mathématiques contiennent en définitive peu de symboles et que l'implicite tient beaucoup de place. Il y a des conventions et des notations propres à chaque discipline mathématique, et dont le caractère subtil implique une signification différente selon le contexte. Certaines notions restent par ailleurs vagues, car elles constituent des éléments de culture partagée des mathématiques. Dès lors, il devient assez complexe de s'assurer que l'assistant de preuve prenne bien en compte tous ces paramètres. Il est donc assez fastidieux de formaliser une preuve car il faut beaucoup détailler pour que l'assistant puisse accepter la preuve. Herman Geuvers, chercheur en informatique, parle ainsi d'un gap entre les preuves telles qu'elles sont publiées dans les revues et les preuves compréhensibles pour un ordinateur.

L'enjeu de l'accessibilité de l'assistant de preuve n'est pas seulement lié à la compréhension et la vérification. L'accessibilité est intimement liée à la communication et au langage. Théo Zimmermann a ainsi souligné qu'une preuve est avant tout "un objet de communication", la preuve doit pouvoir être compréhensible et claire pour pouvoir faire consensus. Le critère de conviction est ainsi un des principaux attributs de la preuve selon Tymoczko. Assia Mahboubi souligne ainsi qu'il reste difficile pour "l'oeil humain" de se convaincre d'une preuve dans le langage formel de l'assistant.

Herman Geuvers opère quant à lui une distinction entre convaincre et expliquer. Il souligne le fait que les preuves mathématiques "traditionnelles" attribuent autant d'importance au détail mathématique en tant que tel qu'à l'explication, puisque la conviction est liée à la compréhension de celui qui parcourt la preuve. Il écrit ainsi que les assistants de preuve "vérifient bien mais expliquent mal", le problème réside dans la communication. Robert Pollack va dans le même sens en exprimant le fait que la conviction en une preuve relève d'une dimension intimement personnelle, qu'il n'est donc pas possible de complètement formaliser. Pour lui, la conviction en une preuve par informatique soulève deux problèmes principaux : un problème formel qui relève de la justesse des calculs et des liens logiques entre les propositions, et un problème informel, qui relève du consensus, de la croyance en la preuve. Pollack souligne bien l'importance de la confiance et de la compréhension en l'assistant de preuve : en effet, l'acceptation de la preuve passe en premier par la confiance en l'assistant, qui est plus facile à obtenir que la compréhension de la preuve elle-même.

Callude et Müller détaillent ainsi des "symptômes de compréhension" pour matérialiser la distinction entre les deux notions. Pour ce qui est des preuves formelles, la compréhension implique pour eux la capacité à modifier le programme si celui ci ne fonctionne pas par exemple. La compréhension est ainsi pour eux le principal obstacle aux preuves formelles, car il n'est pas possible de vérifier humainement la preuve. Cela renforce donc l'importance de la clarté et l'accessibilité des assistants de preuve, qui deviennent les seuls accès possibles à la compréhension de la preuve. C'est pour cette raison que les deux chercheurs plaident pour le développement d'"environnements actifs de preuve" (active proof environments), constitués d'un assistant de preuve (type Coq) et d'une interface intelligente. Cela permettrait aux utilisateurs de questionner les preuves formelles pour en obtenir une meilleure compréhension. Ils suggèrent pour cette interface l'automatisation de chaque étape de preuve, la construction d'analogies et d'exemples, le développement de preuves alternatives et d'illustrations visuelles. Les suggestions montrent ainsi que la compréhension, par extension la conviction d'une preuve, joue sur de nombreux tableaux, qui concourent tous à rendre l'assistant plus accessible.

De manière plus concrète, des solutions sont déjà développées pour permettre l'utilisation de Coq par les domaines civils, comme l'industrie. Nicolas Tabareau, chercheur à l'Inria, travaille sur les moyens d'amener l'industrie à utiliser un assistant de preuve comme Coq. En 2015, le chercheur s'est vu octroyer une bourse du Conseil Européen de Recherche (ERC) pour étudier comment les récents travaux de Vladimir Voevodsky sur la théorie des types peuvent permettre de développer Coq. Dans cette optique, un compilateur formellement vérifié du language de l'assistant de preuve est déjà opérationnel, et permet d'apporter une preuve aux industriels que le programme utilisé se comportera de manière conforme à la sémantique du code source. Dans un entretien, le chercheur raconte que son projet suscite beaucoup d'intérêt dans la communauté scientifique, et que son travail s'effectue en collaboration active avec le créateur de Coq, Thierry Coquand. Le but est de pouvoir créer une nouvelle version de Coq, pour que le logiciel puisse être enseigné en école d'ingénieur et utilisé en recherche et développement.

Le paradoxe de l'accessibilité

Rendre accessible un assistant de preuve tel que Coq confronte les spécialistes à un certain paradoxe. En voulant développer l'assistant de preuve afin que le script final et que son utilisation soit plus lisible et intelligible, le risque de bugs peut potentiellement être augmenté. En effet, développer autour du noyau de l'assistant induit forcément une probabilité d'erreurs plus grande. Cependant, pour altérer le fonctionnement du programme, il faudrait que le bug potentiel soit exploité de telle sorte à rendre le résultat final invalide. Cela correspondrait par exemple à faire croire à l'utilisateur qu'il a démontré ce qu'il cherchait, alors que c'est tout autre chose que le logiciel a prouvé. Assia Mahboubi et Théo Zimmermann relativisent ainsi le risque, en expliquant que la probabilité d'une telle occurrence est infinitésimale.

Il nous a paru au premier abord étonnant de rencontrer la notion d'élégance sur un sujet de recherche portant sur les preuves mathématiques. Pourtant, cette notion est restée en filigrane du développement de la controverse autour du théorème des quatre couleurs, et également au cours des entretiens que nous avons pu réaliser. La notion d'élégance peut paraître curieuse dans la mesure où elle fait intervenir une dimension assez subjective, floue et relativement "accessoire". Ce sont des qualificatifs qui semblent contradictoires avec la fameuse rigueur et la neutralité mathématique qui font des sciences mathématiques un isolat au sein du reste des "sciences dures". Le mathématicien Cédric Villani met à ce titre bien en évidence l'importance des considérations esthétiques en mathématiques : "ll n'y a pas un jour qui se passe dans la vie d'un mathématicien sans qu'il se dise que tel argument est beau ou pas beau. J'ai déjà entendu dire, et c'est peut-être vrai, que les mathématiciens utilisent les mots élégance et beauté plus que tous les autres."

Ainsi, si l'élégance n'est pas un critère exigé et formel de preuve, c'est un critère informel qui conditionne d'une certaine manière, de manière consciente ou non, l'acceptation de la preuve, l'adhésion et le consensus de la communauté sociale des mathématiciens. S'il n'existe pas de définition précise de l'élégance, certains critères sont cependant récurrents. Une preuve élégante a tendance à n'utiliser que peu de résultats préalables, à être courte, et à utiliser une méthode généralisable pour résoudre d'autres problèmes semblables. Lors de notre rencontre avec David Aubin, ce dernier a appuyé sur cette dimension de l'élégance: "La méthode brutale qui consiste à vérifier tous les cas un après l'autre est une méthode qui ne plaît pas beaucoup aux mathématiciens en général". Est élégant pour lui le fait d'utiliser des méthodes très générales, permettant à partir du même raisonnement de résoudre un ensemble de cas très différents.

"Les mathématiques ne possèdent pas seulement la vérité, mais la beauté suprême, une beauté froide, austère, comme celle d'une sculpture." (Bertrand Russell)

La recherche d'une preuve plus noble, plus élégante est ainsi un des principaux moteurs de la recherche d'une preuve du 4CT depuis 1976. Il est alors aisé de comprendre l'engouement et l'espoir suscité par le "fer à cheval" de Shimamoto, qui à partir d'un simple dessin pensait avoir prouvé le 4CT. Il pensait en effet avoir trouvé une configuration D-réductible dont l'existence était incompatible avec l'existence d'une carte penta chromatique. La déception fut grande parmi les mathématiciens quand sa configuration fut invalidée par le programme informatique de Dürre. Encore aujourd'hui, alors même que la vérification de Georges Gonthier a permis de créer un consensus sur la preuve de 1995 du 4CT, certains mathématiciens continuent encore de chercher une preuve manuelle, plus élégante.

Lors de nos entretiens, nous avons eu l'occasion d'interroger des scientifiques de différents domaines vis-à-vis de leur perception d'une preuve élégante.

Selon Assia Mahboubi, au delà de la dimension esthétique, l'élégance en mathématique pourrait recouvrir le fait d'acquérir par le raisonnement et l'analyse une connaissance précise et profonde des concepts manipulés, quand "on a compris quelque chose de plus sur les objets qui sont en jeu" : l'élégance rejoint ici le caractère explicatif de la preuve. Si sa définition de l'élégance était assez vague, Assia Mahboubi avait plus de facilité à nous donner des exemples de ce qui n'était pas élégant. Par ailleurs, elle soulignait également la dimension subjective de l'élégance, qu'elle a illustré avec l'expérience de son oral d'agrégation. En effet, sa méthode de réponse à la question posée avait été critiquée par le jury. Elle avait choisi une méthode faisant intervenir un outil extérieur au problème, tandis que le jury suggérait plutôt l'exploitation de la structure des objets présents dans le problème. Elle avait pourtant une "raison personnelle de trouver cela [son choix] élégant".

Pour l'informaticien Théo Zimmermann, la question de l'élégance est plutôt secondaire : le plus important selon lui est que la preuve soit juste. Dans le cas des preuves formelles, l'élégance est secondaire puisque la relecture est inutile. Il suggère ainsi que l'élégance est intimement liée à la conviction d'une preuve. Si l'élégance est secondaire, il souligne cependant le fait que la publication de preuves postérieures, plus élégantes, est toujours intéressante. En effet, l'élégance permet de "rendre la preuve plus claire". L'élégance relève avant tout d'un effort de l'auteur pour mettre en avant tel ou tel aspect de la preuve ou méthode utilisée. Le travail de Théo Zimmermann pour faciliter l'accessibilité de Coq va dans le sens du développement de preuves formelles plus élégantes.

Pour Cédric Villani, la notion d'élégance est partie intégrante de la conception de la preuve, dans son architecture même, et non pas d'un travail a posteriori pour la rendre élégante. "L'élégance en mathématiques, c'est de trouver quelque chose d'inattendu, qui s'imbrique bien dans un fil directeur, s'intègre dans le reste en faisant une combinaison harmonieuse. Face à un océan de possibilités, plutôt que d'aller au hasard, vous vous laissez guider par ce qui semble la voie la plus belle pour trouver votre chemin."

La controverse sur les preuves informatisées a également muté en une réflexion sur le caractère humain des mathématiques. En effet, de nombreux mathématiciens mentionnent ce caractère éminemment humain et social des mathématiques ; déjà en 1976, Paul Halmos et Daniel Cohen évoquent "l'essence des mathématiques en tant qu'activité dans laquelle la compréhension personnelle et humaine est centrale". Cette vision des mathématiques se retrouve également en filigrane dans nos entretiens et dans de nombreux articles étudiés. Ainsi, William Thurston, mathématicien médaille Fields en 1982, affirme que pour lui, "les mathématiques sont l'une des activités humaines les plus gratifiantes intellectuellement". En particulier, les mathématiciens sont très sensibles au caractère humain de la preuve, comme l'exprime David Aubin lors de notre entretien: "J'ai l'impression que la plupart des mathématiciens restent aujourd'hui très attachés à une façon humaine de faire la preuve". Cet attachement peut s'expliquer du fait du côté créatif de la preuve en mathématiques et de l'importance de l'intuition, faculté éminemment humaine, dans le processus de réflexion et de construction de la preuve.

De fait, à cause de ce caractère humain et social des mathématiques, certains mathématiciens peuvent avoir des réticences à utiliser des outils informatiques dans les preuves. Ainsi, David Aubin explique que, malgré la place de plus en plus importante de l'ordinateur à la fois dans le calcul et la théorie, "l'inertie des pratiques de la communauté [mathématique] est très forte", et l'utilisation d'un ordinateur pour faire des preuves reste très marginale. Pour Jean-Jacques Szczeciniarz, cela s'explique par la peur de perdre le contrôle de l'objet mathématique utilisé, mais aussi à cause "du sentiment d'être dépossédé des ses propres facultés intellectuelles par un objet étranger". Ainsi, alors que l'ordinateur est de plus en plus utilisé en calcul du fait de logiciels comme Maple ou Mathematica et qu'il est également capable de produire de la théorie, l'Homme a d'autant plus peur de perdre prise sur l'aspect créatif et humain des mathématiques. Par ailleurs, comme le rappelle Assia Mahboubi : "Les personnes qui ont choisi de faire de la recherche en mathématiques, c'est parce qu'ils aiment la partie créative, […] on aime bien se poser des questions et essayer de jouer avec les constructions mathématiques pour faire avancer les choses". Ainsi, les mathématiciens peuvent vouloir garder le contrôle sur cette partie créative, c'est-à-dire la production de théorie. En particulier, Pierre-Evariste Dagand évoque le sort des logiciens qui non seulement ressentent, pour certains, "une névrose car ils ont l'impression d'être des moins-que-mathématiciens", mais ont d'autant plus peur de se voir remplacer par les outils informatiques.

Cependant, pour Assia Mahboubi et Théo Zimmermann, du fait de l'aspect éminemment créatif et humain des preuves, celles-ci ne pourront jamais se passer de l'intervention du mathématicien : "La place de l'humain reste énorme dans les preuves formelles informatisées". Cela est dû d'une part à cette intuition, cet aspect créatif nécessaire dans la preuve, et que l'ordinateur n'est pas capable de générer: "Pour l'instant, je ne crois pas que la créativité mathématique sera supplantée" (Assia Mahboubi). Mais cela est également dû au fait qu'une preuve traverse le champ des mathématiques pour utiliser différents concepts nécessaires, ce que la machine ne fait pas vraiment: "les machines ne sont pas capables de trouver automatiquement, on a besoin d'exploiter la connaissance accumulée par les mathématiciens au fur et à mesure de leurs recherches, et retraduire cette connaissance dans une preuve formelle". Dans cette perspective, l'Homme reste nécessaire dans la construction de preuves.

Un exemple, à la croisée de la question de l'élégance et de celle du caractère humain des mathématiques, est particulièrement intéressant. En 2015, une preuve de la conjecture de la discrépance de Erdös fait grand bruit : en effet, celle-ci a été réalisée avec l'aide de l'ordinateur, et surtout pèse environ 13 gigaoctets, soit plus que le contenu de Wikipédia ! Néanmoins, un an plus tard, le mathématicien Terence Tao est parvenu à démontrer cette même conjecture de manière traditionnelle, à la main. De même, il serait tout à fait possible qu'il existe une preuve manuelle et "élégante" du théorème des quatre couleurs. Selon Alan Bundy, la prochaine étape pour résoudre le problème informel de la preuve informatique du 4CT serait de démontrer qu'il n'existe pas de preuve plus courte, mais cela est difficilement décidable.

Vladimir Voevodsky émet l'hypothèse qu'un mathématicien démontrera l'incohérence du système arithmétique de premier ordre conformément à ce que Gödel a démontré dans ses théorèmes d'incomplétude. En conséquence, les mathématiciens ont besoin de fondations sur lesquelles construire des preuves que l'on peut accepter en dépit du fait que l'arithmétique puisse être incohérente. Selon le mathématicien, la réponse se trouve dans la théorie des types. Dans cette théorie, tout objet est fonction. La preuve d'une formule n'est pas une séquence de déductions d'axiomes menant à un résultat. La preuve est une fonction comme n'importe quel objet mathématique. C'est notamment sur cette théorie qu'est fondé l'assistant de preuve Coq. L'idée de Vladimir Voevodsky est de formaliser l'ensemble des mathématiques existantes dans le cadre de la théorie des types, afin de ne travailler qu'à partir de ce qui est vrai et non à partir d'un système d'axiomes qui peut se révéler inconsistant.

Le problème principal à ce projet est la disparité entre l'égalité comme elle existe en mathématique et comme elle se définit dans la théorie des types. En théorie des types, on considère que deux termes sont égaux s'ils correspondent syntaxiquement à la même chose, alors qu'en mathématique, on s'intéresse à l'égalité sémantique. Autrement dit : l'objet mathématique qui se trouve derrière la syntaxe. Cette différence a de profondes implications. En théorie des types, si deux fonctions calculent la même chose mais sont programmées différemment, alors on ne peut pas prouver qu'elles sont égales. Cette limitation constitue un frein important à l'interopérabilité, par exemple quand on veut importer les développements effectués par quelqu'un d'autre.

Selon Nicolas Tabareau, chercheur à l'Inria spécialiste de Coq, l'avancée réalisée par Voevodsky est d'avoir proposé une extension de la théorie des types par des concepts homotopiques. "Pour la première fois, cela permet d'avoir la vraie notion d'égalité dans les assistants de preuve. L'apport de Voevodsky, c'est d'avoir exhibé en un unique axiome ce que doit vérifier l'égalité pour qu'elle devienne sémantique. Tout le monde s'accorde à dire qu'avec cet axiome, dit d'univalence, on récupère tout ce qu'on a envie d'avoir. En particulier l'égalité des fonctions quelle que soit leur syntaxe. Un des enjeux du projet de l'Inria consiste donc à remplacer l'axiome par un contenu calculatoire dans la théorie. En effet, on ne veut pas certifier les preuves avec des axiomes mais avec ce qui est vrai dans la théorie."

L'enjeux de ces prochaines années sera donc la démocratisation de cette nouvelle manière de certifier des résultats mathématiques en les formalisant entièrement en langage informatique. Selon Assia Mahboubi, cette démocratisation des assistants de preuve mettra sûrement fin aux derniers grands débat autour des preuves géantes formalisées en langage informatique.