Philosophie mathématique : enjeux, débats (table ronde et discussion générale)

• Baptiste Mélès
• Brice Halimi (Paris Cité, SPHere)
• Frédéric Patras (CNRS)
• Paola Cantù (CNRS, Centre Gilles Gaston Granger)

Les enjeux des librairies mathématiques (La formalisation des mathématiques dans Lean)

• Antoine Chambert-Loir

Le développement de la librairie Mathlib au sein du logiciel de formalisation mathématique Lean vise explicitement à fournir un corpus cohérent et efficace des bases des mathématiques permettant d'y mener la formalisation de projets de recherche contemporains.Même si des projets similaires, mais moins médiatisés, existent pour d'autres logiciels, Mathlib est souvent comparée au projet qu'avait mené Bourbaki depuis les années 1940. En mettant ces deux projets en regard, j'essayerai de dégager quelques visions philosophiques ou pragmatiques qui les sous-tendent tous deux, puis de réfléchir aux écueils qui pourraient les menacer l'un ou l'autre.

Le développement de l'axiomatique euclidienne : Partie 1 (Le développement de l'axiomatique euclidienne)

• Vincenzo de Risi (SPHere)

**Tracer des figures sur l'eau : origine et signification des postulats d'Euclide** Les deux séances aborderont le thème de l'histoire de la pensée axiomatique de l'Antiquité à l'époque moderne. Plus précisément, la première séance traitera de la naissance de la pensée axiomatique dans les écrits d'Aristote et d'Euclide, et proposera une interprétation dialectique et inférentielle des postulats des Éléments d’Euclide.

Le naturalisme en philosophie des mathématiques 1 (Le naturalisme en philosophie des mathématiques)

• Marianna Antonutti Marfori (IHPST)

Exposé TBA 1

Exposé TBA 2

Le développement de l'axiomatique euclidienne : Partie 2 (Le développement de l'axiomatique euclidienne)

• Vincenzo de Risi (SPHere)

**Le fondement des axiomes : l'idéal scientifique au Moyen Âge et à l'âge classique** Les deux séances aborderont le thème de l'histoire de la pensée axiomatique de l'Antiquité à l'époque moderne. La deuxième sèance montrera certaines transformations de l'épistémologie de l'axiomatique qui ont eu lieu au Moyen Âge et au début de l'époque moderne, et comment elles ont déterminé de manière décisive les études de la révolution scientifique, jusqu'à la découverte des géométries non euclidiennes au 19e siècle.

Les travaux philosophiques et mathématiques de Pierre Cartier 1 - Philosophie (Pierre Cartier, mathématiques et philosophie)

• Frédéric Patras (CNRS)

Que vient faire la philosophie dans l'histoire des mathématiques ? (table ronde) (Que vient faire la philosophie dans l'histoire des mathématiques ?)

• Hourya Benis-Sinaceur (IHPST)

Les travaux philosophiques et mathématiques de Pierre Cartier 2 - Mathématiques (Pierre Cartier, mathématiques et philosophie)

• Frédéric Patras (CNRS)

Le naturalisme en philosophie des mathématiques 2 (Le développement de l'axiomatique euclidienne)

• Marianna Antonutti Marfori (IHPST)

Librairies mathématiques — une nouvelle Babel ? (La formalisation des mathématiques dans Lean)

• Antoine Chambert-Loir

Je voudrais réfléchir ici à la langue dans laquelle nous faisons des mathématiques, d'abord au sens commun, puis au sens du vocabulaire, presque toujours implicite à nos raisonnements, de la théorie des ensembles. De fait, les librairies de mathématiques formalisées utilisent plutôt (mais pas uniquement) un autre langage, celui de la théorie des types qui, par certains aspects, est plus proche de notre discours dans lequel les « types » des objets mathématiques empêchent d'écrire certaines relations : par exemple, quand bien même un nombre réel peut être défini, au sein de la théorie des ensembles, comme une coupure (Dedekind), c'est-à-dire un ensemble de nombres rationnels. il fait rarement sens d'écrire l'égalité d'un nombre réel et d'un ensemble de nombres entiers. Et si plusieurs systèmes formels ont droit de cité, pourront-ils communiquer l'un avec l'autre ?

Exposé TBA 3

Exposé TBA 4

Exposé TBA 5

Exposé TBA 6

Exposé TBA 7