FRAL - Programme franco-allemand en Sciences humaines et sociales

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

Formalisme, formalisation, intuition en mathématiques

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

L’étude de l'interaction entre les théories mathématiques informelles et leur formalisation.

L’objectif du projet est l’étude de l'interaction entre les théories mathématiques informelles et leur formalisation. Réfléchir sur cette interaction signifie réfléchir sur la pratique mathématique et sur ce qui la rend rigoureuse, et comment ce dynamisme génère différentes formes de compréhension. Nous nous proposons donc d'étudier le lien entre différents niveaux de compréhension et la notion de rigueur en mathématiques. <br />En étudiant ces formes de compréhension mathématique, le projet s'appuiera sur des analyses philosophiques et logiques d'études de cas à partir de l'histoire de la pratique mathématique, afin de construire une nouvelle image convaincante de la relation entre la formalisation et la pratique mathématique informelle. La notion de rigueur formelle (dans le sens de la théorie de la preuve) a été largement étudiée en philosophie et en logique, bien que le rôle épistémique du processus de formalisation soit actuellement absent. Nous soutenons que la rigueur formelle est mieux comprise comme une abstraction dynamique des arguments mathématiques informellement rigoureux. <br />Une des principales conséquences de cette enquête sera de montrer que le processus d'acquisition de la compréhension mathématique est beaucoup plus complexe que ne le prétendent les conceptions philosophiques actuelles.

La principale méthodologie de recherche pour ce projet est la réflexion philosophique, menée soit individuellement soit par le biais de discussions communes (séminaires, ateliers, conférences). La réflexion philosophique est combinée à l'analyse logique et historique, afin de fournir un compte rendu philosophique de l'interaction entre la formalisation et la compréhension qui rend compte de la recherche mathématique telle qu'elle se fait dans la pratique mathématique.
L'analyse philosophique et logique des études de cas de l'histoire des mathématiques est cruciale pour le projet de deux façons. Premièrement, l'histoire des mathématiques fournit des études de cas éclairantes pour illustrer les niveaux de compréhension. Deuxièmement, nous considérons également l'histoire des disciplines formelles comme un exemple du rôle épistémologique qu'elles jouent dans la pratique mathématique ordinaire. La logique mathématique est elle-même une discipline mathématique, et donc analogue à d'autres disciplines de ce type en étant née d'un processus de formalisation de certains aspects de la pratique mathématique.

Le fait le plus marquant a été sans aucun doute la présentation de notre projet devant la communauté internationale du domaine lors du 16e Congrès Internationale de Logique, Méthodologie et de Philosophie des Sciences qui s’est tenu à Prague en août 2019. Le symposium, organisé par notre post-doc du projet Maté Szabo, était suivi par une audience très nombreuse et a provoqué un intérêt qui s’exprimait par des intentions de coopérations.
Deux exemples d’avancées scientifiques prometteuses discutées largement dans l’équipe française :
1° Question : Est-il pertinent de parler en mathématiques pures d'expériences de pensée ?
Réponse : Dans la hiérarchie dynamique des formalismes, les instances de preuve et de construction des formalismes de niveau n-1 peuvent être considérées comme des réalisations d'expériences mathématiques par rapport à des preuves «rigoureuses« et des constructions de niveau n. Dans les expériences de pensée mathématiques, nous faisons sur la base d'expériences mathématiques une hypothèse supplémentaire concernant des possibilités épistémiques en utilisant la fonction iconique (intuitive) de l'exemplification.
2° Question : Qu’est-ce que rend formelle une certaine théorie informelle,
et vice versa, Qu’est-ce qui fait qu'une théorie formelle est l'interprétation d’une théorie
informelle ?
Réponse : L'introduction d'un nouveau moyen d'expression implique une forme de refonte d'un ancien corpus de théorie et cela permet aux mathématiciens de se concentrer sur les mêmes caractéristiques du contenu d’un tel corpus mathématique, et de le rendre essentiel dans le cadre de la nouvelle théorie impliquant ce nouveau moyen d'expression. Une forme de compréhension mathématique résulte si une théorie mathématique donnée ‘informelle’ est interprétée par une nouvelle théorie, où ce n'est qu'une forme de refonte qui permet d'améliorer le contrôle sur les contenu pertinent originaire.

Un workshop conjoint avec le projet ANR PROGRAMme est prévu pour le mois de décembre. Il s'agit de discuter des collaborations possible entre les deux projets en matière de formalisation des algorithmes en maths et informatique, et des relations entre preuves et programmes informatiques. Un de deux coordinateurs (MP) est en train de terminer un livre (qui sera soumis aux éditions Springer, Synthese Library) dont la rédaction a énormément bénéficié des discussions internes au projet. le livre porte sur la notion d'économie épistémique,, dont la conception dépend de manière essentielle de la vision des relations entre connaissance informelle et formalisation développée dans le projet. Ce sera un des résultats majeurs du projet.

Publications multipartenaires
A) International
1° Revues
Marianna Antonutti Marfori
• (2018) « Human Effective Computability” (with L. Horsten).?Philosophia Mathematica 27(1):61–87. DOI: doi.org/10.1093/philmat/nky011 <b

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.

Coordinateur du projet

Monsieur Gerhard HEINZMANN (Laboratoire d'Histoire des Sciences et de Philosophie - Archives henri-Poincaré)

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

IECL Institut Elie Cartan de Lorraine
IHPST Institut d'Histoire et de Philosophie des Sciences et des Techniques
MCMP Munich Center of Mathematical Philosophy
LHSP-AP Laboratoire d'Histoire des Sciences et de Philosophie - Archives henri-Poincaré

Aide de l'ANR 450 287 euros
Début et durée du projet scientifique : avril 2018 - 36 Mois

Liens utiles