Un logiciel conçu pour vérifier des démonstrations mathématiques est en train de changer la façon dont on construit l’intelligence artificielle. Lean 4, créé par le Brésilien Leonardo de Moura, n’a rien d’un gadget universitaire. C’est un outil qui force les machines à prouver qu’elles ont raison, ligne par ligne, sans tricher.
Un assistant de preuve devenu langage de programmation
Lean existe depuis 2013, mais sa quatrième version a tout changé. Là où les versions précédentes restaient cantonnées aux labos de maths, Lean 4 est aussi un vrai langage de programmation fonctionnel. On peut écrire du code, le compiler, et en même temps prouver formellement qu’il fait ce qu’il prétend faire. AWS l’utilise déjà pour vérifier Cedar, son système d’autorisation qui gère les accès de millions d’utilisateurs, selon la documentation officielle du projet.
La bibliothèque Mathlib, maintenue par la communauté, dépasse le million de lignes de mathématiques formalisées. Algèbre, topologie, probabilités : tout y passe. Et un projet encore plus ambitieux est en cours, la formalisation complète du dernier théorème de Fermat.
Pourquoi l’IA s’y intéresse
Le problème des grands modèles de langage, c’est qu’ils hallucinent. Ils génèrent du texte plausible sans garantie de vérité. Lean offre l’inverse : un cadre où chaque affirmation doit être prouvée avant d’être acceptée.
Des chercheurs ont créé LeanDojo, un environnement open source présenté à NeurIPS 2023, qui permet aux modèles d’interagir directement avec Lean pour démontrer des théorèmes. Leur système, ReProver, utilise un LLM augmenté par de la recherche de prémisses dans Mathlib. Résultat : il surpasse GPT-4 sur ces tâches avec un seul GPU et une semaine d’entraînement, rapportent les auteurs dans leur publication sur arXiv.
L’ACM a d’ailleurs décerné son prix SIGPLAN 2025 à l’équipe de Lean, en soulignant son « impact significatif sur les mathématiques, la vérification logicielle et matérielle, et l’IA ».
À lire aussi
Le pont entre rigueur mathématique et code IA
Lean 4 n’est pas le seul assistant de preuve. Rocq (ex-Coq), Isabelle et d’autres existent depuis des décennies. Mais Lean a un avantage : il est à la fois un prouveur et un langage compilé performant. On peut écrire l’algorithme et sa preuve dans le même fichier. Ça change la donne pour la vérification de systèmes critiques, du contrôle aérien aux smart contracts.
La Lean Focused Research Organization, créée en 2023 avec le soutien de fondations et d’acteurs privés, travaille sur l’automatisation des preuves et la montée en charge du système. L’objectif affiché : rendre la vérification formelle accessible au-delà du cercle des mathématiciens.
Et après ?
Faut-il s’attendre à ce que les futurs ChatGPT prouvent leurs réponses avant de les envoyer ? On n’y est pas encore. Mais la convergence entre LLM et assistants de preuve ouvre une piste fascinante : celle d’une IA qui ne se contente pas de deviner juste, mais qui sait expliquer pourquoi elle a raison. Le chemin est long, certes. Mais pour une fois, on a un outil qui permet de vérifier chaque pas.
