Des assistants de preuves pour l’analyse réelle et numérique; un focus sur Rocq: de la recherche à l’enseignement et vice versa (1)

• Micaela Mayero (Université Sorbonne Paris Nord)

Room: Amphithéâtre Poisson Les outils de preuves formelles, issus des recherches en logique, ont pris de l’ampleur ces dernières décennies. Nous présenterons succinctement ces outils, leurs évolutions ainsi que leurs fondements théoriques. Les preuves formelles sont utilisées et développées à la fois dans le domaine de l’enseignement, principalement en mathématiques et en informatique, et de la recherche, et ces dernières années, parfois de manière coordonnée. Nous présenterons ces deux aspects en faisant un focus sur l’analyse réelle et l’analyse numérique en Rocq. Nous nous appuierons régulièrement sur des exemples.

Du calcul et des machines dans les preuves (1)

• Benjamin Werner (INRIA & École polytechnique)

Room: Amphithéâtre Poisson L’ordinateur est une machine capable d’exécuter précisément un algorithme donné. Cela en fait naturellement un outil mathématique. Je parlerai en particulier de deux rôles: - Vérifier des preuves formelles. C’est le principe des assistants de preuves qui sont le thème de ces journées. - Effectuer des calculs complexes, numériques ou symboliques, qui sont hors de portée de l’humain. Nous regarderons comment certains formalismes, comme la théorie des types sous-jacente à Rocq et Lean, permet de concilier ces deux aspects à travers des preuves comportant une part de calcul importante. Parmi ces preuves, il y a le théorème des quatre couleurs, dont nous présenterons quelques aspects. Dans une dernière partie, je présenterai des travaux plus récents sur une interface graphique et gestuelle pour construire des preuves formelles de manières (parfois) plus rapide ou intuitive. Ces travaux ouvrant, je l’espère, des pistes nouvelles pour la pédagogie des mathématiques.

Une présentation de Lean et Mathlib à base d'exemples mathématiques (1)

• Sébastien Gouézel (CNRS - IRMAR)

Room: Amphithéâtre Poisson Les assistants de preuve sont des langages dans lesquels on explique à un ordinateur des preuves mathématiques, l'ordinateur se chargeant de vérifier que le passage d'une ligne à la suivante respecte toujours les règles de la logique. Cela permet entre autres avantages de garantir quasiment à 100% la correction des démonstrations. Je présenterai l'assistant de preuves Lean et sa bibliothèque de mathématiques formalisées Mathlib, avec un point de vue de mathématicien praticien (et donc sans parler du tout du fonctionnement interne des assistants de preuve) : quelles différences de point de vue faut-il avoir quand on démontre un résultat sur papier ou quand on le formalise, quels sont les types d'arguments les plus difficiles de chaque côté, quels sont les écueils à éviter, etc. Je m'appuierai principalement sur des exemples concrets. Je démontrerai puis expliquerai la formalisation d'un théorème sur les vecteurs de translation asymptotique de fonctions 1-lipschitziennes. Ensuite, je me concentrerai sur la notion de fonction $C^n$, telle qu'exposée dans les livres ou dans les cours, puis telle que formalisée dans Mathlib -- il y a des différences significatives entre les deux, qui illustrent bien les particularités des mathématiques formalisées.

Des assistants de preuves pour l’analyse réelle et numérique; un focus sur Rocq: de la recherche à l’enseignement et vice versa (2)

• Micaela Mayero (Université Sorbonne Paris Nord)

Room: Amphithéâtre Poisson Les outils de preuves formelles, issus des recherches en logique, ont pris de l’ampleur ces dernières décennies. Nous présenterons succinctement ces outils, leurs évolutions ainsi que leurs fondements théoriques. Les preuves formelles sont utilisées et développées à la fois dans le domaine de l’enseignement, principalement en mathématiques et en informatique, et de la recherche, et ces dernières années, parfois de manière coordonnée. Nous présenterons ces deux aspects en faisant un focus sur l’analyse réelle et l’analyse numérique en Rocq. Nous nous appuierons régulièrement sur des exemples.

Du calcul et des machines dans les preuves (2)

• Benjamin Werner (INRIA & École polytechnique)

Room: Amphithéâtre Poisson L’ordinateur est une machine capable d’exécuter précisément un algorithme donné. Cela en fait naturellement un outil mathématique. Je parlerai en particulier de deux rôles: - Vérifier des preuves formelles. C’est le principe des assistants de preuves qui sont le thème de ces journées. - Effectuer des calculs complexes, numériques ou symboliques, qui sont hors de portée de l’humain. Nous regarderons comment certains formalismes, comme la théorie des types sous-jacente à Rocq et Lean, permet de concilier ces deux aspects à travers des preuves comportant une part de calcul importante. Parmi ces preuves, il y a le théorème des quatre couleurs, dont nous présenterons quelques aspects. Dans une dernière partie, je présenterai des travaux plus récents sur une interface graphique et gestuelle pour construire des preuves formelles de manières (parfois) plus rapide ou intuitive. Ces travaux ouvrant, je l’espère, des pistes nouvelles pour la pédagogie des mathématiques.

Une présentation de Lean et Mathlib à base d'exemples mathématiques (2)

• Sébastien Gouézel (CNRS - IRMAR)

Room: Amphithéâtre Poisson Les assistants de preuve sont des langages dans lesquels on explique à un ordinateur des preuves mathématiques, l'ordinateur se chargeant de vérifier que le passage d'une ligne à la suivante respecte toujours les règles de la logique. Cela permet entre autres avantages de garantir quasiment à 100% la correction des démonstrations. Je présenterai l'assistant de preuves Lean et sa bibliothèque de mathématiques formalisées Mathlib, avec un point de vue de mathématicien praticien (et donc sans parler du tout du fonctionnement interne des assistants de preuve) : quelles différences de point de vue faut-il avoir quand on démontre un résultat sur papier ou quand on le formalise, quels sont les types d'arguments les plus difficiles de chaque côté, quels sont les écueils à éviter, etc. Je m'appuierai principalement sur des exemples concrets. Je démontrerai puis expliquerai la formalisation d'un théorème sur les vecteurs de translation asymptotique de fonctions 1-lipschitziennes. Ensuite, je me concentrerai sur la notion de fonction $C^n$, telle qu'exposée dans les livres ou dans les cours, puis telle que formalisée dans Mathlib -- il y a des différences significatives entre les deux, qui illustrent bien les particularités des mathématiques formalisées.

Travaux pratiques LEAN

• Patrick Massot

Room: Amphithéâtre Poisson