CONFERENCE / RESEARCH SCHOOL

Lean for the curious mathematician 2024
Lean pour mathématiciens 2024

25 – 29 March, 2024

INTRANET FOR ORGANIZERS

Scientific Committee 
Comité scientifique 

Anne Baanen (Vrije University Amsterdam)
Johan Commelin (University of Freiburg)
Sébastien Gouëzel (CNRS – Université Rennes 1)
Heather Macbeth (Fordham University)
Assia Mahboubi (INRIA Rennes Bretagne Atlantique)

Organizing Committee
Comité d’organisation

Riccardo Brasca (Université Paris Cité)
Antoine Chambert-Loir (Université Paris Cité)
Maria Ines De Frutos Fernandez (Imperial College London)
Filippo Nuccio Mortarino Majno di Capriglio (Université Jean Monnet Saint-Étienne)

IMPORTANT WARNING:  Scam / Phishing / SMiShing ! Note that ill-intentioned people may be trying to contact some of participants by email or phone to get money and personal details, by pretending to be part of the staff of our conference center (CIRM).  CIRM and the organizers will NEVER contact you by phone on this issue and will NEVER ask you to pay for accommodation/ board / possible registration fee in advance. Any due payment will be taken onsite at CIRM during your stay.

Formalisation is the process of digitalising mathematical results, teaching them to a computer. It has several benefits, the most obvious being the verification of the correctness of theorems beyond any reasonable doubt, starting from the axioms. Formalisation is becoming a more and more popular activity for mathematicians. The existence of huge libraries of formalised mathematics will have an important impact in the daily life of the working mathematician, who will soon be able to formalise their own research and have databases of theorems, rather than databases of papers. In the next few years, computer programs for formalization — called proof assistants — will also be able to help in mathematical research, taking care of “routine” calculations and similar problems.
   Many proof assistants can be used to formalise mathematics. Two of the most commonly used today by “standard mathematicians” are Lean and Coq, and the conference will mainly focus on the first. Lean comes with a vast library of formalised mathematics, mathlib. The existence of such a library allows one to work on contemporary mathematics. For example, one spectacular recent result has been the formalisation, by Commelin, Topaz and several other people, of one of the main results by Clausen and Scholze about condensed mathematics. This is cutting edge mathematics, using several theories, from functional analysis to homological algebra.
   The meeting’s main goal is to introduce mathematicians to Lean and to formalisation in general. There will be several talks, given by Lean experts, to explain the basics and provide examples, as well as many “practice sessions”, where participants will use Lean in real world situations. Taking advantage of the presence of many French scientists working in Coq, we also plan to invite some of them to offer three or four talks about this other proof assistant, mainly discussing differences, similarities and potential collaborations. The conference’s focus will at any rate be about formalising “standard mathematics”, and in particular it will neither be about foundations of mathematics nor programming. At the end of the week people will have drafts of results that can soon be included into mathlib, tangibly contributing to the development of formalised mathematics. We expect that the conference will enable people to start formalising modern mathematics, and their own research in the near future. Lean for the Curious Mathematician 2024 will be part of the series États de la Recherche SMF of the French Mathematical Society.

La formalisation est le procès de numérisation de résultats mathématiques, dans le but de les expliquer à un ordinateur. Parmi les avantages, le plus évident est la vérification de l’exactitude des preuves au-delà de toute doute, et ceci en ne partant que des axiomes. Le thème de la formalisation est en train de se révéler de plus en plus important pour les mathématiciens et l’existence de grandes bibliothèques numériques de mathématiques formalisées aura un impact croissant dans le travail des mathématiciens, qui auront à leur disposition une vaste collection de théorèmes, plutôt qu’une base de données d’articles. Dans les années à venir, les logiciels de formalisation, appelés « assistants de preuve», pourront aussi aider les mathématiciens dans leur démarche de recherche, en accomplissant des tâches routinières de calcul ou de raisonnement basique.
   Plusieurs assistants de preuve peuvent être utilisés pour formaliser des mathématiques. Deux des plus répandus à l’heure actuelles parmi les « mathématiciens classiques » sont Lean et Coq, et la conférence se concentrera principalement sur le premier. 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 qui a récemment été atteint est la formalisation, complétée 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.
   Le but principal du colloque sera celui d’introduire des chercheurs en mathématiques à Lean et à la formalisation en général. D’une part, il y aura plusieurs exposés, donnés par des experts de Lean, d’introduction aux fondamentaux et aux exemples principaux ; d’autre part, on prévoit des séances d’exercice et entraînement où les utilisateurs seront menés à utiliser Lean pour formaliser des énoncés classiques. En nous appuyant sur la présence de nombreux chercheurs français travaillant en Coq, nous prévoyons aussi d’inviter certains d’entre eux afin de proposer 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. La conférence sera néanmoins centrée autour de la formalisation de mathématiques « classiques » plutôt qu’autour des fondements des mathématiques ou des langages de programmation. À la fin de la semaine les participants auront des ébauches de projets de formalisation qui pourront être intégrés dans mathlib dans un temps raisonnable, en leur permettant de manière concrète de participer au développement des mathématiques formalisées. Nous nous attendons que la conférence permettra à de nombreux mathématiciens de formaliser des mathématiques modernes, ou même leurs propres travaux dans un futur proche. Lean pour mathématiciens 2024 fera partie de la série États de la Recherche SMF.

SPEAKERS

Alex Best (King’s College London)
Chris Birkbeck (University of East Anglia)
Kevin Buzzard (Imperial College London)
Moritz Doll (University of Bremen)
Floris van Doorn (Université Paris-Saclay)
Frédéric Dupuis (Université de Lorraine)
María Inés de Frutos Fernández (Boston University)
Georges Gonthier (Microsoft Research)
Alena Gusakov (University of Delaware)
Florent Hivert (Université Paris-Saclay)
Marie Kerjean (CNRS – Université Sorbonne Paris Nord)
Amelia Livingston (King’s College London)
Jireh Loreaux (Southern Illinois University)
Patrick Massot (Université Paris-Saclay)
Guillaume Melquiond (Université Paris-Saclay)
Oliver Nash (Imperial College London)
Eric Rodriguez (King’s College London)

SPONSORS