Le 30 juin, Mistral a publié Leanstral 1.5, un modèle open weight sous Apache 2.0 dédié à la preuve formelle en Lean 4. Nous l’avons poussé une semaine sur trois cas concrets. Verdict : à intégrer si vous vivez dans le monde de la vérification formelle, à ignorer complètement autrement.
Pour résumer
- Leanstral 1.5 est un MoE 119B / 6,5B actifs, contexte 256k, Apache 2.0, gratuit dans Mistral Labs
- Il résout 587 des 672 problèmes de PutnamBench, un benchmark de math formels sérieux
- Utile pour un labo, un éditeur crypto ou un prof de math ; overkill pour la majorité des équipes tech
Ce qui change avec Leanstral 1.5
Leanstral 1.5 est la suite directe du premier Leanstral, le modèle Mistral dédié à Lean 4, un langage de vérification formelle utilisé par les mathématiciens et une frange d’ingénieurs sécurité. Deux évolutions comptent : la taille et la licence.
Côté taille, Mistral passe à une architecture Mixture of Experts. Le modèle compte 119 milliards de paramètres au total, dont 6,5 milliards actifs à chaque forward pass. Le compromis est classique : plus de capacité, latence contrôlée, coût d’inférence maîtrisé.
Le contexte grimpe à 256 000 tokens. C’est loin du strict minimum pour manipuler des preuves qui embarquent leurs dépendances, leurs lemmes et le code source associé. Ce point à lui seul débloque des cas d’usage que la version précédente ne supportait pas proprement.
Côté licence, Mistral maintient l’Apache 2.0. Les poids sont téléchargeables sur Hugging Face, l’usage commercial est autorisé, et le modèle est également accessible gratuitement dans Mistral Labs pour ceux qui n’ont pas les GPU nécessaires. Le geste vise clairement la communauté chercheurs et la vérification embarquée.
La stratégie recoupe celle d’autres labs qui montent en spécialisation verticale. Anthropic ouvre Claude Science pour les labos scientifiques avec un ciblage recherche. Mistral joue la même carte, plus étroite : la vérification mathématique et logicielle.
Notre test sur trois cas concrets
Nous avons poussé Leanstral 1.5 sur trois scénarios que les équipes techniques rencontrent réellement, à défaut de faire de la math pure. Le but était de mesurer où le modèle est utile hors du contexte académique.
Premier cas : formaliser un contrat de smart contract simplifié (transfert conditionnel, absence de reentrancy, invariant sur la somme totale). Sur ce type d’objet, Leanstral 1.5 propose des lemmes intermédiaires cohérents et pilote Lean 4 pour valider chaque étape. Le gain de temps par rapport à une écriture manuelle est réel : nous estimons deux à trois fois plus rapide pour un ingénieur qui connaît déjà Lean.
Deuxième cas : audit de propriétés sur du code Rust critique (structure de données concurrente, allocation mémoire, invariants d’un pool). Le modèle a signalé plusieurs cas où une preuve était trop faible et a proposé une version renforcée. Sur les 57 dépôts référencés par Mistral, le lab revendique 47 propriétés violées et 11 bugs réels remontés. Notre expérience colle : le taux de vraies détections est solide.
Troisième cas : reformuler en Lean 4 une preuve littéraire de complexité O(log n) sur une implémentation AVL tree. C’est un exemple que Mistral met en avant. Nous avons pu répliquer la preuve avec une intervention humaine minimale. La partie autoformalisation (traduire une démonstration écrite en mots vers un code Lean vérifiable) marche mieux qu’attendu.
Où le modèle fatigue : dès que l’énoncé s’éloigne des schémas classiques (théorèmes en topologie exotique, preuves qui demandent de choisir la bonne astuce parmi cinq mille possibles), Leanstral 1.5 propose des chemins qui n’aboutissent pas. Le score PutnamBench de 587 sur 672 est excellent, mais les 85 problèmes ratés sont exactement ceux qui demandent un vrai raisonnement créatif.
Face à un modèle open comme MiniMax M3, poussé sur le raisonnement général, Leanstral se distingue précisément par sa verticalité. M3 est bien meilleur pour discuter d’un problème math en langage naturel. Leanstral est bien meilleur pour produire du Lean valide.
À voir également sur Horizon :
- Zuckerberg agents IA : plus lents que prévu chez Meta
- Sakana AI : notre test de l’IA dont tout le monde parle
- Prototype IA SpaceX : téléphone en approche, Musk dément
Notre verdict : à intégrer ou à zapper selon votre métier
Nous recommandons Leanstral 1.5 dans trois cas de figure précis. Le premier est un labo académique ou industriel qui travaille déjà avec Lean 4. Le modèle gagne un temps considérable et évite les impasses de raisonnement. L’installation locale sur un cluster GPU sérieux tient en une journée.
Deuxième cas : un éditeur critique en sécurité ou en blockchain qui audite du code où l’erreur coûte cher. Vérification formelle sur des composants clés, intégrée dans la CI : Leanstral 1.5 change la vitesse d’itération. Ce n’est pas un remplacement des audits humains, c’est un pré-filtre qui remonte les vraies alertes.
Troisième cas : un enseignant ou formateur en math qui prépare des exercices formalisés pour ses étudiants. Autoformaliser un cours entier en Lean 4 devient possible sans y passer un semestre. Le retour sur investissement est immédiat pour tout programme universitaire.
Pour tout le reste, Leanstral 1.5 est overkill. Un marketeur, un chef de produit, un consultant en transformation IA n’en retirera rien. La vérification formelle n’est pas un besoin de leur métier et un chat généraliste type Sonnet 5 ou GPT 5.6 leur rend mille fois plus service.
La grille de lecture est simple. Leanstral 1.5 est un outil précis pour un usage précis. Il ne cherche pas à remplacer un chat généraliste, il pose une brique sur un marché que peu d’acteurs adressent. Chez Mistral, le pari est cohérent avec la stratégie open weight verticale que d’autres labs comme DeepSeek explorent aussi côté inférence.
Le vrai enjeu pour Mistral est de convertir ce succès technique en adoption enterprise. Une preuve formelle certifiée par Leanstral et vérifiée par Lean 4 pourrait devenir un livrable standard chez certains éditeurs critiques d’ici douze mois. C’est là que se joue la valeur commerciale du modèle.
Affaire à suivre sur Horizon.
