Projet FFIUM

Marco Panza

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

 

Projet ANR-DFG franco-allemand. Partenaires : Institut Elie Cartan de Lorraine, LHSP-AP Laboratoire d'Histoire des Sciences et de Philosophie - Archives Henri-Poincaré, MCMP Munich Center of Mathematical Philosophy

 

mai 2018-avril 2021

 

Ce projet étudie l'interaction entre les théories mathématiques informelles (TMI) et leur formalisation et soutient que ce dynamisme génère plusieurs formes distinctes 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.

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.