L’essentiel
- Anthropic annonce que Claude a achevé le mois dernier la formalisation d’une preuve mathématique majeure en Lean.
- Lean est un assistant de preuve : chaque étape passe ou casse, sans relecteur humain dans la boucle.
- La validation d’une grande démonstration par la communauté peut demander des années ; la formalisation vise à compresser ce délai.
- L’enjeu dépasse les mathématiques : c’est l’un des rares terrains où un agent travaille très longtemps avec un verdict objectif à chaque pas.
Vérifier une grande démonstration mathématique prend des mois, parfois des années, et repose sur des relecteurs qui la reprennent ligne à ligne. Anthropic vient d’annoncer que Claude a achevé la formalisation d’une preuve majeure dans Lean, un langage dont le correcteur n’a ni fatigue ni indulgence.
Traduire une démonstration dans un langage exécutable
Le langage Lean appartient à la famille des assistants de preuve : des langages dans lesquels on écrit un énoncé mathématique et sa démonstration sous une forme entièrement explicite. Chaque déduction doit se ramener à des règles élémentaires que le programme sait contrôler.
L’analogie la plus juste est celle du compilateur. Un mathématicien qui rédige un article laisse des « il est clair que » et des étapes jugées évidentes ; un relecteur les accepte ou les conteste, avec sa fatigue et ses angles morts. Dans Lean, rien de tel : ou bien la preuve compile, ou bien elle échoue, et le message d’erreur pointe l’endroit exact où le raisonnement cède.
Formaliser revient donc à traduire. On part d’une démonstration écrite en français mathématique et on la réécrit dans ce langage, en s’appuyant sur Mathlib, la bibliothèque communautaire qui rassemble déjà des dizaines de milliers de résultats formalisés. Un travail long, ingrat, et qui a jusqu’ici mobilisé des équipes entières de volontaires.
Un terrain où la note ne se négocie pas
Presque tout ce qu’un modèle de langage produit est évalué par un humain, ou par un autre modèle chargé d’imiter son jugement. Une réponse bien tournée l’emporte souvent sur une réponse juste, et les méthodes d’alignement héritent de ce biais : on finit par optimiser la satisfaction du juge.
La formalisation supprime le juge. Une preuve en Lean est acceptée ou refusée par un noyau de vérification réduit, indépendant du modèle qui l’a écrite. Aucune élégance de formulation ne rattrape un lemme faux. Pour entraîner et pour mesurer des agents, ce signal binaire, disponible sans limite, vaut cher.
Des mois de travail, personne au-dessus de l’épaule
La difficulté ne tient pas à une étape isolée mais à leur nombre. Une formalisation sérieuse, ce sont des milliers de lemmes intermédiaires à poser, à nommer, à réutiliser, avec une architecture qui tienne sur la durée. Un modèle brillant sur une question isolée échoue régulièrement sur ce type de chantier : il perd le fil, refait ce qui existe déjà, s’enferre dans une voie sans issue.
Ce que teste Anthropic tient à l’endurance plus qu’aux mathématiques : un agent capable d’avancer des jours, voire des semaines, sur un objectif unique, sans qu’un humain vienne recadrer chaque itération. Lean fournit l’ingrédient qui manque partout ailleurs, une boucle de retour immédiate, dense et impossible à berner. Google DeepMind avait déjà branché un modèle sur Lean avec AlphaProof, qui a atteint le niveau de la médaille d’argent à l’Olympiade internationale de mathématiques 2024. La différence tient à l’échelle : un problème d’olympiade tient en un énoncé, une formalisation complète s’étale sur des milliers de lemmes.
Le raisonnement reste humain, la garantie s’arrête à l’énoncé
Deux nuances à garder en tête avant d’extrapoler. Formaliser une démonstration existante ne revient pas à la découvrir : le raisonnement vient des mathématiciens, la machine le rend exécutable. La frontière compte, même si la seconde tâche est loin d’être mécanique.
Ensuite, la garantie porte sur ce qui a été écrit, pas sur ce qu’on croit avoir écrit. Si l’énoncé de départ est mal traduit, Lean validera consciencieusement une preuve du mauvais théorème. Le langage accepte aussi des trous assumés (le mot-clé sorry) et l’ajout d’axiomes : une preuve qui compile se juge donc aussi sur ce qu’elle a supposé. La vérification est mécanique, la confiance reste affaire de relecture humaine.
Hors des mathématiques, la même dépendance au vérificateur
Rien de tout cela ne se limite aux théorèmes. Un agent va aussi loin que le vérificateur qu’on lui donne, et un vérificateur utile est automatique, rapide et sans appel :
- une suite de tests qui échoue franchement, plutôt qu’un avis « ça a l’air bon » ;
- des types stricts et un schéma de données qui refusent l’à-peu-près ;
- un environnement d’exécution réel, plutôt qu’une relecture par un second modèle.
Là où ce vérificateur manque, l’autonomie s’arrête vite, quel que soit le modèle employé. C’est la ligne de partage entre les tâches qu’on délègue sur la durée et celles qu’il faut continuer à surveiller pas à pas.
Les mathématiciens, eux, jugeront sur un autre critère : la lisibilité. Une démonstration formalisée que plus personne ne relit devient une boîte noire certifiée exacte, ce qui n’est pas tout à fait l’idéal d’une discipline bâtie sur l’explication.
Mon avis
Ce chantier m’intéresse moins pour les mathématiques que pour ce qu’il dit des limites actuelles de l’autonomie : un agent tient la distance quand quelque chose lui répond non, tout de suite, sans discussion possible. Retirez le vérificateur, et les mêmes modèles dérivent en quelques heures. J’attends donc les prochains gains d’autonomie là où un vérificateur existe déjà, le code compilé, les tests, les schémas de données, avant de les voir ailleurs. Le reste attendra qu’on sache fabriquer des juges aussi durs que Lean.
