Colloque - Formalisation des mathématiques et types dépendants - Riccardo Brasca : Progrès récents dans la formalisation de la théorie des nombres

Épisode de Informatique et sciences numériques (2024-2025) - Thierry Coquand par Collège de France · 2 juin 2025 · 47 min

Collège de France

Thierry Coquand

Informatique et sciences numériques (2024-2025)

Année 2024-2025

Colloque - Formalisation des mathématiques et types dépendants - Riccardo Brasca : Progrès récents dans la formalisation de la théorie des nombres

Riccardo Brasca

Maître de conférences, université Paris Cité

Résumé

Dans cet exposé, nous discuterons de l'état actuel de la formalisation de la théorie des nombres moderne dans mathlib, la bibliothèque mathématique de Lean. Nous mettrons en avant les avancées récentes, les principaux défis qui ont été relevés, ainsi que les implications plus larges de ce travail. Nous aborderons également les perspectives d'avenir et les applications potentielles, en soulignant comment ces développements contribuent à l'écosystème croissant des mathématiques formalisées.

Riccardo Brasca

Riccardo Brasca a obtenu son doctorat à l'université de Milan (Italie) en 2012, avec une thèse portant sur les formes modulaires p-adiques. Après son doctorat, il a effectué deux postdoctorats, l'un au Max-Planck-Institut für Mathematik à Bonn et l'autre à l'École normale supérieure de Lyon. Depuis 2013, il est maître de conférences à l'université Paris-Cité et depuis 2020 il travaille en formalisation des mathématiques.

Autres épisodes de « Informatique et sciences numériques (2024-2025) - Thierry Coquand »

• Colloque - Formalisation des mathématiques et types dépendants - Denis-Charles Cisinski : La logique des catégories supérieures 2 juin 2025
• Colloque - Formalisation des mathématiques et types dépendants - Pierre-Marie Pédrot : Pour s'asseoir sur les fondations 2 juin 2025
• Colloque - Formalisation des mathématiques et types dépendants - Assia Mahboubi : Preuves formelles mutatis mutandis 2 juin 2025
• Colloque - Formalisation des mathématiques et types dépendants - Antoine Chambert-Loir : Sur la formalisation des puissances divisées 2 juin 2025
• 08 - Théorie des types dépendants et formalisation des mathématiques : Modalités et modèles de la théorie des types 19 mai 2025
• 07 - Théorie des types dépendants et formalisation des mathématiques : Espaces d'Eilenberg-MacLane et cohomologie 12 mai 2025
• 06 - Théorie des types dépendants et formalisation des mathématiques : Modèles de la théorie des types et du principe d'univalence 5 mai 2025
• 05 - Théorie des types dépendants et formalisation des mathématiques : Le mystère de l'égalité ; la notion de type comme généralisation de la notion d'ensemble 28 avril 2025
• 04 - Théorie des types dépendants et formalisation des mathématiques : Théorie des types et théorie des ensembles 7 avril 2025
• 03 - Théorie des types dépendants et formalisation des mathématiques : Univers, paradoxes et normalisation 31 mars 2025
• 02 - Théorie des types dépendants et formalisation des mathématiques : Déduction naturelle et modèles 24 mars 2025
• 01 - Théorie des types dépendants et formalisation des mathématiques : La théorie des types, de Russell à de Bruijn 17 mars 2025
• Leçon inaugurale - Thierry Coquand : La théorie des types, de Russell aux assistants à la démonstration 13 mars 2025

Tous les épisodes de Informatique et sciences numériques (2024-2025) - Thierry Coquand · Plus de podcasts Éducation