Le langage Lean
Démontrer qu’un programme est correct
Comment être certain qu’un programme informatique ne contient aucune erreur critique ? Dans l’industrie logicielle classique, la réponse repose principalement sur les tests. Mais tester un programme ne garantit jamais qu’aucun bug ne subsiste.
Lean propose une autre approche. Plus qu’un langage de programmation, c’est aussi un assistant de preuve capable de vérifier mathématiquement qu’un programme informatique fonctionne correctement. Longtemps cantonnée à la recherche théorique, cette promesse se trouve aujourd’hui au cœur d’enjeux scientifiques, industriels et sociétaux majeurs.
Le code évolue constamment. Les preuves doivent donc pouvoir s’adapter aux réécritures du logiciel.
Leonardo de Moura, chercheur en informatique et créateur de Lean, architecte en chef et co-fondateur du Lean Focused Research Organization (Lean FRO)
Concrètement, le système fonctionne comme un immense jeu de construction mathématique. Le chercheur écrit des hypothèses, applique des règles de raisonnement appelées « tactiques », puis Lean vérifie automatiquement chaque étape. Si une erreur apparaît, elle est immédiatement détectée. Cette approche est appelée « preuve formelle » et transforme la manière de concevoir des logiciels critiques. Jusqu’à récemment, ces méthodes restaient extrêmement coûteuses en temps et en expertise, nécessitant beaucoup d’efforts de programmation. Mais l’arrivée de l’IA change la donne, celle-ci permettant de faire baisser l’effort nécessaire.
Leonardo de Moura, chercheur en informatique et créateur de Lean, architecte en chef et co-fondateur du Lean Focused Research Organization (Lean FRO).
Une communauté internationale pour sécuriser le numérique
Créé par le chercheur en informatique Leonardo de Moura, Lean et les possibilités impressionnantes qu’il offre ont fait émerger une communauté scientifique et industrielle. Porté par Emilio Jesús Gallego Arias, ingénieur de recherche senior au Lean Focused Research Organization (Lean FRO) dont Leonardo de Moura est architecte en chef et co-fondateur, le Lean Paris Meetup a réuni chercheurs, ingénieurs, développeurs et industriels à Mines Paris – PSL autour d’un objectif : permettre aux humains et aux machines de construire des démonstrations mathématiques rigoureuses et des logiciels vérifiés.
Nous voulons créer un lieu où les idées issues de la recherche, de l’industrie et du développement collaboratif puissent se rencontrer et évoluer ensemble.
Emilio Jesús Gallego Arias ingénieur de recherche senior au Lean Focused Research Organization (Lean FRO) et organisateur du Lean Paris Meetup
Pour Mines Paris – PSL, cet événement marque une étape importante dans le développement d’un écosystème scientifique dédié aux méthodes formelles et aux langages de preuve. En associant recherche, formation et partenariats industriels, l’École s’inscrit pleinement dans ce mouvement émergent, exigeant et prometteur.
Emilio Jesús Gallego Arias, ingénieur de recherche senior au Lean Focused Research Organization (Lean FRO) et organisateur du Lean Paris Meetup.
Un lieu de rencontre entre recherche, industrie et communauté open source
Cette approche connaît aujourd’hui une accélération spectaculaire. Des entreprises comme Amazon Web Services (AWS), Microsoft, Google ou Mistral AI utilisent déjà l’outil Lean pour vérifier des bibliothèques cryptographiques (c’est-à-dire des ensembles de programmes réalisant des opérations de chiffrement pour protéger les données et garantir leur confidentialité), des compilateurs (des logiciels qui traduisent le code écrit par les développeurs en langage machine compréhensible par les ordinateurs) ou des systèmes informatiques critiques (dont une erreur pourrait avoir de graves conséquences).
L’un des projets emblématiques est Signal Shot, une initiative lancée conjointement par l’application de messagerie Signal, la Beneficial AI Foundation et la Lean FRO. Son but est de vérifier mathématiquement le protocole de chiffrement de Signal, c’est-à-dire les mécanismes qui protègent les messages des utilisateurs ainsi que le logiciel qui le met en œuvre écrit dans le langage de programmation Rust. Utilisé pour développer des applications sécurisées, Rust est réputé pour sa robustesse et sa capacité à limiter certaines failles informatiques. Quand plus de 100 millions de personnes utilisent Signal dans le monde, démontrer formellement que ces systèmes fonctionnent correctement devient un enjeu majeur de confiance numérique.
L’essor de Lean s’explique aussi par la formalisation informatique des mathématiques contemporaines, ce qui est une évolution majeure. Aujourd’hui Mathlib, la bibliothèque mathématique de Lean, rassemble plus de 270 000 théorèmes formalisés et plus de deux millions de lignes de code. Elle mobilise plus de 750 contributeurs à travers le monde. Pour la recherche, l’enjeu n’est pas seulement de vérifier des démonstrations, mais aussi de transformer la manière de collaborer.
La preuve par l’IA
De plus, une véritable convergence se dessine entre IA et mathématiques formelles. Lors du Meetup, Roman Soletskyi, chercheur chez Mistral AI, a présenté Leanstral, agent open-source spécifiquement conçu pour Lean 4. Son objectif est d’aider à écrire du code Lean et à construire plus rapidement des démonstrations formelles. Cette évolution s’inscrit dans un contexte d’accélération spectaculaire des usages de l’IA dans les mathématiques et la vérification logicielle. Dès lors, le défi n’est plus seulement de produire du code ou des preuves, mais de pouvoir les valider rigoureusement.
Aujourd’hui, des agents d’intelligence artificielle sont déjà capables d’écrire des preuves en Lean, de proposer des optimisations ou encore de restructurer automatiquement des bibliothèques entières. On peut évoquer l’exemple des dix agents d’IA ayant réussi à construire en un week-end un langage spécialisé, accompagné de preuves complètes de sûreté.
Mais cette automatisation renforce aussi, en parallèle, la nécessité de disposer de mécanismes de validation particulièrement robustes. Cette idée résume l’un des grands enjeux contemporains de la preuve formelle : alors que les systèmes logiciels deviennent de plus en plus autonomes et générés par des IA, la confiance ne peut plus reposer uniquement sur des tests classiques.
Une tradition de recherche ancienne à Mines Paris – PSL
Si Lean apparaît aujourd’hui comme une technologie émergente, les recherches qui l’ont rendue possible s’inscrivent dans une histoire scientifique plus ancienne, à laquelle Mines Paris – PSL contribue depuis plusieurs décennies. Au CRI, les travaux sur les systèmes de typage des langages de programmation remontent aux années 1990. Ces recherches constituent une partie des fondements théoriques des assistants de preuve modernes.
Le CRl, en particulier grâce à l’apport de Emilio Jesús Gallego Arias, alors chercheur postdoctoral au sein du laboratoire, a notamment travaillé, dès 2013 sur Rocq, anciennement Coq, dans le cadre du projet ANR Faust Environment Everyware : une solution ubiquitaire pour le traitement audionumérique portable et multiplateforme – FEEVER, coordonné par le chercheur émérite du CRI Pierre Jouvelot et consacré au traitement audionumérique. Ce logiciel permet de :
- exprimer des raisonnements mathématiques de manière formelle, c’est-à-dire très rigoureuse et sans ambiguïté ;
- vérifier automatiquement si une démonstration mathématique est correcte ;
- assister les chercheurs dans la construction de preuves, en les guidant étape par étape ;
- produire automatiquement des programmes informatiques « certifiés », c’est-à-dire garantis comme corrects par des méthodes mathématiques.
Lean est fortement inspiré de Rocq, mais il bénéficie aujourd’hui d’un contexte technologique nouveau, marqué par l’essor de l’IA et des besoins industriels en vérification logicielle.
Pierre Jouvelot, chercheur émérite au CRI
Olivier Hermant, chercheur au CRI, participe ainsi au développement de Dedukti, un vérificateur universel de preuves co-développé avec Inria Paris-Saclay. L’objectif est notamment de permettre l’interopérabilité entre différents assistants de preuve comme Lean, Rocq ou Isabelle/HOL.
Former aux systèmes de preuve de demain
L’ITN contribue à structurer cet écosystème. Fin 2025, l’institut organisait déjà un atelier « 100 % Lean » destiné aux enseignants en informatique et à plusieurs partenaires techniques et industriels.
Ces ateliers ont vocation à faire découvrir très concrètement des technologies en évolution rapide et au potentiel prometteur.
Sébastien Boisgérault, enseignant-chercheur au CAOR
Au-delà de la recherche et des partenariats industriels, l’École entend prendre part au mouvement en intégrant Lean à son offre de formation. Cette évolution témoigne d’un changement plus large dans la manière de former les ingénieurs. Demain, il ne suffira peut-être plus seulement de savoir programmer ; il faudra aussi être capable de démontrer mathématiquement qu’un système logiciel est correct, robuste et sécurisé. Pour l’ITN, cette dynamique s’inscrit pleinement dans sa mission de diffusion et d’expérimentation des technologies numériques émergentes.
Il existe aujourd’hui des synergies particulièrement impactantes autour de ces technologies. Le domaine reste relativement réduit, mais son potentiel disruptif impose d’y prêter attention, car ces travaux ont des applications très concrètes. Les outils formels développés autour de la méthode B, par exemple, une méthode formelle qui permet le raisonnement sur des systèmes complexes ainsi que le développement logiciel, ont servi à concevoir le logiciel de la ligne 14 du métro parisien.
Une nouvelle culture de la preuve
Dans un contexte où les systèmes numériques deviennent omniprésents, que ce soit dans les transports, la santé, la cryptographie ou encore l’IA, la capacité à démontrer mathématiquement qu’un programme fonctionne correctement devient un enjeu stratégique. Si l’IA produit de plus en plus de code et que les infrastructures numériques gouvernent des systèmes critiques, la question n’est plus seulement de créer des logiciels performants, mais de prouver leur fiabilité.
La tenue du Lean Paris Meetup à Mines Paris – PSL illustre ainsi une volonté plus large : faire émerger un point de rencontre entre recherche académique, innovation industrielle et nouveaux usages. Mines Paris – PSL affirme là son ambition de contribuer activement à une nouvelle culture scientifique de la preuve, où les mathématiques formelles deviennent un outil central de la confiance numérique.
Dans un monde où les logiciels pilotent des infrastructures critiques et où l’intelligence artificielle génère de plus en plus de code dont la correction reste toujours discutable, la capacité à vérifier formellement les systèmes informatiques de demain pourrait devenir l’un des enjeux technologiques majeurs des prochaines décennies.
Pour aller plus loin
