Terence Tao explique aux mathématiciens la fiabilité de Lean et le rôle de l'IA

Le 9 octobre 2026, Terence Tao a publié sur son blog un billet intitulé « What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI ». Le titre désigne clairement son public : les mathématiciens professionnels qui s'intéressent à la vérification formelle et aux systèmes d'IA capables d'écrire des preuves. Sur Hacker News, le billet a recueilli 53 points et 7 commentaires. Seul le lien est arrivé dans notre flux, sans le texte. Nous ne résumons donc pas les arguments de l'auteur. Nous décrivons ci-dessous le contexte dans lequel ce type de billet apparaît, et ce qui le rend important.

Pourquoi la question de la fiabilité est devenue pratique

Lean est né en 2013 comme projet de Leonardo de Moura chez Microsoft Research. Aujourd'hui, c'est un outil de travail pour de vastes projets collectifs. Fin 2023, Tao lui-même a participé à la formalisation de la conjecture PFR, qui a pris environ trois semaines. En 2024, il a coordonné l'Equational Theories Project : il s'agissait de déterminer 22 028 942 implications entre 4694 identités sur les magmas. Sans automatisation ni vérification formelle, ni les humains ni les relecteurs n'auraient pu venir à bout d'un tel volume.

En parallèle, les modèles de langage se sont mis à travailler dans Lean. En juillet 2024, AlphaProof de Google DeepMind a résolu quatre des six problèmes de l'IMO et obtenu 28 points sur 42. Elle produisait ses preuves en Lean. Depuis, la question « peut-on se fier à ce qui sort d'une telle chaîne ? » ne relève plus de la philosophie des mathématiques, mais du travail quotidien.

Où passe la frontière de la confiance

Lean dispose d'un petit noyau qui vérifie chaque terme de la preuve. Les tactiques, l'automatisation et le code généré par un modèle se trouvent à l'extérieur de ce noyau. S'ils se trompent, le noyau rejette simplement le résultat. C'est ce qui rend l'association avec l'IA attrayante : une hallucination dans une preuve est détectée mécaniquement.

Il reste des points où la confiance doit être évaluée séparément :

• Énoncé du théorème. Le noyau confirme que l'énoncé tel qu'il est écrit a été démontré. C'est à l'humain de juger s'il correspond à ce qui était voulu.
• Définitions. Une définition imprécise dans la bibliothèque ou dans le fichier vide de sens le théorème démontré.
• Axiomes. Lean s'appuie sur `propext`, `Classical.choice` et `Quot.sound`. La commande `#print axioms` indique lesquels sont utilisés.
• `sorry`. C'est un bouchon qui tient lieu de preuve. Un fichier qui en contient compile, mais le théorème n'est pas démontré.
• `native_decide`. Cette tactique ajoute le compilateur à la base de confiance, et `Lean.ofReduceBool` apparaît dans la liste des axiomes.
• Implémentation du noyau. Il existe des vérificateurs indépendants, par exemple lean4checker et des revérifications tierces, qui réduisent le risque d'erreur dans le noyau lui-même.

Ce que change l'IA

Avant l'arrivée des modèles, la principale limite était le travail du formalisateur. Le modèle en allège une partie, car il produit des centaines de candidats à la preuve. La vérification par le noyau reste peu coûteuse. En revanche, une seconde tâche passe au premier plan : s'assurer que l'énoncé formel dit réellement ce que l'auteur avait en tête. Le noyau ne fait pas ce travail, et un modèle qui ajuste la preuve à l'énoncé peut trouver des failles dans l'énoncé lui-même. Exemple typique : l'énoncé est trivialement vrai à cause d'un ensemble vide ou d'une division par zéro mal définie.

On en tire une conclusion pratique : l'audit se déplace des étapes de la preuve vers les conditions du problème. Pour les mathématiciens, il s'agit plutôt d'un changement de compétence que d'une perte de contrôle.

Comment travailler avec ces outils

Si vous comptez utiliser Lean ou un assistant IA dans un travail de recherche, il est utile de suivre une courte marche à suivre :

• Rédigez ou relisez vous-même les énoncés des théorèmes, même si la preuve a été générée par un modèle.
• Avant publication, lancez `#print axioms` et cherchez les `sorry`.
• Vérifiez que les définitions de Mathlib utilisées correspondent à votre compréhension. Pour les cas non standard, écrivez des contre-exemples et des lemmes de vérification.
• Pour les résultats critiques, passez le fichier dans un outil de vérification indépendant.
• Lisez le billet original de Tao. Nous avons fourni ici un contexte ; il vaut mieux chercher ses arguments et ses recommandations à la source.