FFIUM — Formalisme, formalisation, intuition et compréhension en mathématiques : de la pratique informelle aux systèmes formels et retour

Ce projet étudie l'interaction entre les théories mathématiques informelles (TMI) et leur formalisation et soutient que ce dynamisme génère trois formes distinctes de compréhension: 1. Différents types de formalisations fixent les frontières et les dépendances conceptuelles entre les concepts de différentes façons, contribuant ainsi à notre compréhension du contenu d'une TMI. On soutient que cette forme de compréhension d'une théorie informelle est obtenue en la reformulant comme une théorie formelle, ie. en transformant ses moyens expressifs. 2. Dès qu'une théorie formelle est disponible, elle devient un objet de compréhension. Une contribution essentielle à cette compréhension est faite en reconnaissant cette théorie comme une formalisation d'un corpus particulier de mathématiques informelles. On clarifiera cette forme de compréhension par l'étude de modèles singuliers et des classes de modèles révélant les points communs conceptuels sous-jacents entre objets dans les différentes zones de mathématiques. 3. Le troisième niveau concerne la façon dont l'étude des formalisations d'une même zone peut conduire à une transformation du contenu de ces zones et à un changement dans la géographie des mathématiques informelles. En étudiant ces formes de compréhension, on s'appuiera sur des analyses philosophiques et logiques d'études de cas tirés de l'histoire de la pratique mathématique, afin de construire une nouvelle image convaincante de la relation entre formalisation et pratique mathématique informelle. Une des principales conséquences de cette enquête sera de montrer que le processus d'acquisition de la compréhension mathématique est bien plus complexe que ne l'estiment les conceptions philosophiques actuelles. Alors que l'impact de la formalisation sur la pratique mathématique est souvent considéré comme négligeable, on défend l'idée que la formalisation est un outil épistémique qui non seulement impose des limites aux problèmes étudiés dans la pratique, mais produit aussi de nouveaux modes de raisonnement qui peuvent élargir les méthodes standard de la preuve dans différentes zones mathématiques. Réfléchir sur l'interaction entre les TMI et leur formalisation, c'est réfléchir sur la pratique mathématique et ce qui la rend rigoureuse, et comment ce dynamisme génère différentes formes de compréhension. On se propose donc d'étudier le lien entre les trois niveaux de compréhension décrits ci-dessus et la notion de rigueur en mathématiques. La notion de rigueur formelle (dans le sens de la théorie de la preuve) a été très étudiée en philosophie et en logique, bien que le rôle épistémique du processus de formalisation ne soit pas pris en compte. On soutient que la rigueur formelle est mieux comprise comme une abstraction dynamique des arguments mathématiques informellement rigoureux. Ces arguments seront étudiés en analysant des études de cas à partir de différents sous-domaines de mathématiques, afin d'identifier des modèles de raisonnement rigoureux.