4 Décembre 2023

Victor Rabiet (ENS)

De la preuve informelle à la preuve formelle

Malgré une certaine montée en puissance des assistants de preuves ces dernières années,
la majeure partie du travail du mathématicien,
et en particulier ce qu'il publie,
consiste en ce que l'on peut appeler l'élaboration de preuves informelles.

On peut se demander quelle est donc la part épistémique de la dynamique mathématique,
si elle est nécessaire ou non, et quelles conséquences
pourrait-on en tirer pour le développement à venir des mathématiques.

En particulier, nous nous poserons la question de l'intérêt de développer
un formalisme "intermédiaire", qui permettrait d'approcher "par le haut"
une version plus formelle des preuves et des travaux mathématiques usuels.