Formalisation de l'arithmétique dans le système Lean – FALSE

FALSE est un projet fédérant six experts de formalisation mathématique dans l'assistant de preuve Lean, qui travaillent à formaliser certains résultats clés en arithmétique.

Le but de FALSE est celui de progresser vers la formalisation du programme de Langlands, en ayant en vue comme première étape la définition de la représentation galoisienne attachée par Deligne à une forme modulaire. Afin d'avancer vers cet objectif de très longue haleine, quatre thèmes principaux seront développés par les membres de FALSE: la théorie du corps de classes, les formes modulaires p-adiques "à la Serre", les représentations galoisiennes associées aux courbes elliptiques, le formalisme des représentations p-adiques admissibles avec la définition de certains anneaux de périodes apparaissant en théorie de Hodge p-adique. En parallèle de ces quatre directions, le projet propose aussi deux sujets de thèse, portant sur la formalisation de la thèse de Tate et sur l'analyse p-adique.

Le projet s'insère dans le cadre global des avancées récentes en formalisation mathématique, qui est en train de franchir des étapes remarquables en suscitant l'intérêt de la communauté mathématique internationale. Plusieurs équipes ont récemment abouti à la formalisation de résultats très profonds, à partir du Liquid Tensor Experiment proposé par Scholze (auquel trois membres de FALSE ont contribué), à la formalisation de la preuve de la conjecture de Freiman-Ruzsa polynomiale par Tao, aux résultats obtenus par l'IA AlphaProof de Google DeepMind, entraînée en Lean. Les avancées obtenues par FALSE permettront de s'attaquer à des projets de telle ampleur même en théorie algébrique des nombres et en géométrie arithmétique.