Le but principal du colloque sera de proposer une introduction à Lean et à la formalisation en général à l’intention de des chercheurs et chercheuses en mathématiques. La formalisation mathématique est le processus de numérisation de résultats mathématiques — il s’agit en quelque sorte d’expliquer des mathématiques à un ordinateur. Parmi les intérêts d’un tel travail, le plus évident, et celui qui est le plus souvent mis en avant, est la vérification de l’exactitude des preuves au-delà de tout doute : l’ordinateur garantit l’enchaînement logique des démonstrations à partir des premiers axiomes. Ce thème gagne actuellement de l’importance et on peut penser que l’existence de grandes bibliothèques numériques de mathématiques formalisées aura un impact croissant dans le travail des mathématiciens et mathématiciennes, dès lors qu’il met à leur disposition une vaste collection de théorèmes vérifiés, plutôt qu’une base de données d’articles dont les arguments sont parfois insuffisants. Dans les années à venir, les « assistants de preuve », les logiciels de formalisation, pourront également aider les mathématiciens et mathématiciennes dans leur démarche de recherche, en accomplissant des tâches routinières de calcul ou de raisonnement basique.
De nombreux assistants de preuve permettent aujourd’hui de formaliser des mathématiques. Parmi les plus répandus à l’heure actuelle, en particulier pour le développement des « mathématiques classiques », on trouve Coq et Lean, et la conférence se concentrera principalement sur le second. La bibliothèque mathlib est la collection principale des mathématiques formalisées en Lean et elle est déjà très vaste. L’existence d’une telle bibliothèque permet de formaliser des mathématiques modernes de façon efficace. Par exemple, un résultat spectaculaire récemment obtenu est la formalisation par Commelin, Topaz et leur équipe d’un des résultats principaux de Clausen et Scholze sur les mathématiques condensées. Il s’agit de mathématiques profondes et récentes, qui nécessitent de plusieurs théories qui vont de l’analyse fonctionnelle à l’algèbre homologique.
La conférence sera centrée autour de la formalisation de mathématiques « classiques » plutôt qu’autour des fondements des mathématiques ou des langages de programmation. Plusieurs exposés, donnés par des experts de Lean, constitueront une présentation des concepts de base et des exemples principaux.
Nous prévoyons aussi des séances d’exercice et d’entraînement où les utilisateurs seront amenés à utiliser Lean pour formaliser des énoncés classiques. En nous appuyant sur la présence en France de nombreux collègues travaillant en Coq, nous prévoyons aussi d’en inviter certains à présenter trois ou quatre exposés centrés sur cet autre assistant de preuve, principalement afin de discuter des différences, des similitudes et des échanges possibles parmi les communautés.
Les projets de formalisation débutés au cours de cette semaine pourront, à terme, être intégrés dans mathlib. De la sorte, les participantes et participants auront pu participer de manière concrète au développement des mathématiques formalisées. Nous escomptons que la conférence permette à plus de mathématiciennes et mathématiciens de formaliser des mathématiques modernes, voire les inciter à formaliser leurs propres travaux.
Lean pour mathématiciens 2024 est une conférence de la série États de la Recherche SMF.