ROUGH DRAFT authorea.com/104457
Main Data History
Export
Show Index Toggle 6 comments
  •  Quick Edit
  • Adaptation d’un assistant de preuve au besoin de l’utilisateur mathématicien

    Introduction

    Les mathématiques formelles, c’est-à-dire des démonstrations rédigées dans un langage tel qu’un ordinateur soit capable de les vérifier, sont un champ d’études depuis plus de quarante ans (de Bruijn 1970) mais n’ont commencé à attirer une communauté importante d’utilisateurs que très récemment. Les assistants de preuve, qui sont des logiciels qui aident à écrire ce genre de démonstrations, intéressent à la fois la communauté de la certification (logicielle, matérielle) et la communauté mathématique. Cette dernière a, dans un passé récent, produit des démonstrations d’une taille telle qu’elle commence à craindre que la relecture par les pairs ne soit plus suffisante pour garantir la validité d’une démonstration (Hales 2008) (Gonthier 2008) (Univalent Foundations Program 2013). Même s’ils ont atteint un certain niveau de maturité, les assistants de preuve sont encore difficiles à utiliser et les rendre plus accessibles, pour permettre qu’une communauté bien plus importante les utilise, est une préoccupation de plus en plus grande parmi les chercheurs du domaine.

    Cette thèse a pour objectif de faire quelques pas dans cette direction dans le cadre de Coq (The Coq development team 2016), un assistant de preuve dont la communauté d'utilisateurs et l'équipe de développement sont extrêmement actifs et qui est parmi les plus utilisés au monde.

    Vers une bibliothèque collaborative et universelle

    Le premier pas abordé est la question du partage et de la réutilisation des preuves déjà effectuées. En effet, la science se construit par couches successives et cela est particulièrement vrai en mathématiques. Aujourd'hui, l'une des raisons de la difficulté de formaliser des démonstrations difficiles et qu'il faut bien souvent formaliser également les résultats préliminaires sur lesquels elles se basent. Cela n'est pas arrangé par le fait que de nombreuses bibliothèques ont été développées pour Coq, par différentes équipes, de manière indépendante. Elles sont par conséquent incompatibles les unes avec les autres, et bien souvent incomplètes.

    Bien souvent également, des résultats intermédiaires dans des développements plus ou moins courts ne finissent jamais par être partagés sous forme de bibliothèque par leur auteur, ce qui conduit d'autres personnes à les réinventer parfois de manière quasi-identique.

    Faciliter le partage n'est pas pour autant une question aisée ou purement pratique. Elle soulève également un certain nombre de problèmes théoriques intéressants. L'un de ces problèmes est de rendre compatibles des développements indépendants qui ne l'étaient pas.