Leanstral 1.5 arrive avec une promesse très concrète : aider à produire des preuves (et pas seulement du texte) dans Lean 4, en s’appuyant sur une approche d’agent de code. Et surtout, on parle d’un modèle open source dont l’objectif est la démonstration automatisée de théorèmes.
Ce n’est pas “magique” : c’est un système qui tente de résoudre des problèmes formalisés, puis de vérifier ce qu’il propose. Dans l’écosystème Lean, cette différence compte énormément. Ici, l’enjeu n’est pas d’avoir une explication plausible, mais un résultat qui passe la vérification.
Qu’est-ce que Leanstral 1.5, exactement ?
Leanstral 1.5 est un modèle d’agent de code conçu pour Lean 4. Son usage principal est la démonstration automatisée et l’ingénierie de la démonstration : autrement dit, aider à construire des preuves Lean, ou à industrialiser une partie du travail de formalisation.
Les poids du modèle sont annoncés comme disponibles sous licence Apache 2.0. C’est un point important pour les équipes qui veulent expérimenter sans rester dépendantes d’une interface fermée.
Une architecture “mixture-of-experts” pour mieux cibler le calcul
Leanstral 1.5 utilise une architecture de type mixture-of-experts (MoE). Concrètement, l’idée est d’acheminer chaque token vers des sous-réseaux spécialisés. Résultat : on limite la charge de calcul tout en conservant une capacité globale élevée.
Ce choix n’est pas qu’un détail technique. Pour des tâches de preuve, où la structure logique compte, le fait de spécialiser des “experts” peut aider à mieux traiter des sous-problèmes hétérogènes (lemmes, réécritures, instanciations, etc.).
Les performances : 587/672 sur PutnamBench
Pour mesurer ce que vaut un démonstrateur neuronal, il faut des benchmarks qui forcent la formalisation. Ici, PutnamBench joue ce rôle : il s’agit d’un benchmark multilingue inspiré de problèmes de concours, avec des formalisation réalisées à la main.
Sur PutnamBench en Lean 4, Leanstral 1.5 résout 587 des 672 problèmes. C’est un score qui se lit comme une capacité à “tenir la distance” sur un ensemble large et exigeant, plutôt que de réussir quelques cas faciles.
Le modèle établit aussi des records annoncés sur d’autres métriques : 87 % sur FATE-H et 34 % sur FATE-X. L’intérêt, c’est que ces chiffres donnent un aperçu de la robustesse sur des familles de tâches différentes.
Pourquoi PutnamBench est un test sérieux
PutnamBench regroupe 1 724 formalisation issues du concours William Lowell Putnam. En Lean 4, on parle de 672 problèmes formalisés (et il existe aussi des versions en Isabelle et en Coq).
La difficulté vient du fait que la démonstration exige une maîtrise d’un large éventail de sujets de niveau premier cycle. Et surtout, le benchmark est pensé pour être un défi ouvert : les approches existantes ne résolvent qu’une poignée de problèmes, ce qui rend la progression mesurable.
À quoi ça sert, pour un développeur ou un chercheur ?
Leanstral 1.5 n’est pas seulement un “score de benchmark”. Si vous travaillez avec Lean 4, l’intérêt est de réduire le coût de certaines étapes : exploration de pistes de preuve, génération de squelette de démonstration, ou assistance à l’ingénierie logique.
En pratique, ce type d’agent peut aider à :
- accélérer la formalisation en proposant des tentatives de preuves ;
- réduire le temps passé à “chercher” un bon lemme ou une bonne stratégie ;
- améliorer l’itération sur des preuves existantes (ajuster, restructurer, compléter).
Et comme Lean vérifie, vous obtenez un retour binaire : soit la preuve passe, soit elle ne passe pas. C’est exactement le genre de boucle qui rend l’assistance IA utile.
Ce qu’il faut garder en tête : l’IA n’est pas un remplaçant total
Même avec un score élevé, il reste des cas où l’agent ne réussit pas. Et c’est normal : la formalisation mathématique combine intuition, stratégie et savoir-faire. L’IA peut proposer, mais elle ne “comprend” pas au sens humain ; elle optimise une génération de preuves qui doit ensuite être validée.
Le bon réflexe, c’est de voir Leanstral 1.5 comme un coéquipier : il vous aide à avancer, puis vous reprenez le volant quand la preuve devient trop spécifique ou exige une stratégie fine.
Conclusion : une étape claire vers la preuve assistée
Leanstral 1.5 montre une direction nette : des agents capables de produire des preuves Lean 4, avec des performances mesurées sur PutnamBench et des poids disponibles sous Apache 2.0. Si vous faites de la formalisation, c’est une brique à tester pour gagner du temps sur l’ingénierie de démonstration.
La question suivante n’est plus “est-ce que ça marche ?”, mais “dans quels workflows concrets ça devient vraiment rentable ?”.