Preuve formelle : comment un ordinateur vérifie les maths

Début octobre, OpenAI a publié d’un coup des centaines de démonstrations mathématiques produites par son IA (nous en avons parlé ici). Une précision revenait sans cesse dans les commentaires : seule une partie de ces résultats était « vérifiée en Lean ». Et c’est précisément cette partie que les mathématiciens prenaient au sérieux.

Mais que veut dire « vérifié en Lean » ? Pourquoi un logiciel aurait-il plus de crédit qu’un comité de professeurs ? Cette semaine, dans Décryptage IA, on ouvre le capot de la preuve formelle, cette discipline austère qui est en train de devenir, sans bruit, le garde-fou numéro un des IA mathématiciennes.

D’abord, c’est quoi une preuve ?

📘 Définitions pour débutants Une preuve (ou démonstration), c’est un enchaînement d’étapes logiques qui part de choses admises et arrive, sans trou, à une conclusion. Si chaque marche est solide, l’escalier tient. Une preuve formelle, c’est la même chose, mais écrite dans un langage si précis qu’un ordinateur peut vérifier chaque marche de l’escalier, une par une, sans rien laisser passer. Lean est l’un de ces langages, accompagné de son vérificateur. On parle d’assistant de preuve.

Pourquoi en a-t-on besoin ? Parce que les mathématiciens écrivent pour des humains. Dans un article de recherche, on trouve des formules comme « il est clair que » ou « par un argument similaire ». C’est comme une recette de grand-mère qui dit « une pincée de sel » et « cuire jusqu’à ce que ce soit bon » : un cuisinier expérimenté s’en sort, un robot non. Lean, lui, est ce robot pointilleux : il exige les grammes, les degrés et les minutes.

À quoi ça ressemble, concrètement ?

Voici deux minuscules exemples en Lean 4. Le premier dit : « 2 + 2 = 4, et c’est vrai par simple calcul » :

example : 2 + 2 = 4 := rfl

Le second énonce que l’ordre ne compte pas dans une addition de nombres entiers naturels, et s’appuie pour le prouver sur un résultat déjà démontré de la bibliothèque :

theorem mon_addition (a b : Nat) : a + b = b + a := Nat.add_comm a b

La structure est toujours la même : un énoncé (ce qu’on veut prouver), puis une preuve (comment on y arrive). Si tout est cohérent, Lean ne dit rien, ce qui veut dire « accepté ». Au moindre trou, il souligne l’endroit fautif en rouge, et refuse d’aller plus loin. Pas de « presque juste ».

Pour les vraies démonstrations, on ne tape pas chaque micro-étape à la main : des commandes appelées tactiques automatisent les parties fastidieuses. Et surtout, on s’appuie sur Mathlib, une immense bibliothèque collaborative lancée en 2017 : en mai 2025, elle comptait déjà plus de 210 000 théorèmes et 100 000 définitions formalisés. Un peu comme un Lego géant où chaque brique a été contrôlée une fois pour toutes.

Pourquoi faire confiance à une machine ?

Bonne question ! Le vérificateur au cœur de Lean est volontairement petit et simple. On n’a donc pas besoin de croire des milliers de pages de raisonnement : il suffit de croire ce petit noyau, scruté par une communauté entière. Un peu comme en métrologie : plutôt que de relire chaque pièce d’une machine, on fait confiance à un seul instrument de mesure, parfaitement étalonné.

Quatre histoires qui ont tout changé

Problème	Le souci	La vérification formelle
Théorème des quatre couleurs (toute carte peut se colorier avec 4 couleurs)	Démonstration historique reposant sur un programme qui examinait d’innombrables cas : peut-on se fier au programme ?	Vérifié avec l’assistant Coq par Georges Gonthier (Microsoft Research), article disponible en 2005
Conjecture de Kepler (la meilleure façon d’empiler des oranges)	Preuve annoncée en 1998 ; en 2003, les 12 relecteurs se disent « sûrs à 99 % », sans pouvoir tout vérifier	Projet Flyspeck, terminé le 10 août 2014 après environ 11 ans (Isabelle et HOL Light)
Liquid Tensor Experiment	Le médaillé Fields Peter Scholze met la communauté au défi de vérifier un de ses théorèmes clés, fin 2020	Formalisation en Lean, achevée le 14 juillet 2022
Conjecture PFR (Terence Tao et coll.)	Résultat récent, technique	Formalisé en Lean dès 2023, l’année même de sa publication

La leçon de ces épisodes : la preuve formelle sert surtout quand la démonstration est trop longue, trop calculatoire ou trop neuve pour qu’un humain puisse en être certain.

Et ça ne sert pas qu’aux maths

La même technique vérifie aussi des logiciels. L’exemple de référence s’appelle seL4, un noyau de système d’exploitation (le cœur qui gère un ordinateur) d’environ 8 700 lignes de code C. En 2009, ses concepteurs ont démontré formellement que le code suit toujours sa spécification : il ne plante jamais et n’effectue jamais d’opération dangereuse. Pour des systèmes où une panne coûte des vies ou des fortunes, ce genre de garantie vaut de l’or.

Pourquoi l’IA en a tant besoin

Les modèles de langage ont un défaut congénital : ils peuvent halluciner, c’est-à-dire écrire quelque chose de faux avec un aplomb parfait. En mathématiques, c’est rédhibitoire. D’où une idée simple : l’IA propose, Lean dispose. Le modèle est un étudiant brillant mais parfois affabulateur ; Lean est l’examinateur intraitable qui vérifie la copie ligne par ligne.

• 2024 : le système AlphaProof de Google DeepMind démontre des énoncés en Lean au niveau d’une médaille d’argent aux Olympiades internationales de mathématiques.
• Avril 2025 : DeepSeek publie DeepSeek-Prover-V2, un modèle spécialisé dans les preuves en Lean.
• Octobre 2026 : OpenAI publie ses résultats mathématiques en indiquant que beaucoup de preuves sont en cours de formalisation en Lean, et que d’autres le seront au fil du temps.

⚠️ Les vraies limites de la preuve formelle Lean vérifie la preuve, pas la question. Si l’énoncé a été mal traduit en Lean au départ, la preuve sera parfaitement valide… d’autre chose. C’est comme un GPS : il vous mène pile à l’adresse saisie. Faute de frappe dans l’adresse ? Vous arrivez au mauvais endroit, avec une précision impeccable. C’est long et coûteux. Flyspeck a demandé une décennie. Formaliser reste un travail d’expert, même si l’IA commence à l’accélérer. Tout n’est pas encore dans Mathlib. Dans les domaines peu couverts, il faut d’abord construire les briques de base. La confiance n’est jamais absolue. On fait confiance au petit noyau de Lean, aux axiomes choisis et au matériel. C’est très peu, mais ce n’est pas zéro.

💡 Pour essayer vous-même (sans rien installer) Le Lean Playground (live.lean-lang.org) permet de taper du Lean directement dans votre navigateur : copiez-y les deux exemples ci-dessus pour voir Lean les accepter. Pour une initiation ludique, le Natural Number Game, proposé sur le serveur de jeux Lean de l’université de Düsseldorf, fait redécouvrir l’addition et la multiplication sous forme de niveaux à débloquer. Il est en anglais.

À vous la parole

• Feriez-vous davantage confiance à une preuve vérifiée par une machine ou relue par dix experts ?
• Si l’IA produit des preuves que plus aucun humain ne comprend, mais que Lean valide, est-ce encore des mathématiques ?
• Faudrait-il exiger une vérification formelle pour les logiciels des avions, des voitures ou des banques ?