Mistral publie Leanstral 1.5, un MoE spécialisé en preuves Lean 4

Ce n'est pas la course aux paramètres qui rend cette sortie intéressante, mais un ciblage très étroit. Mistral vient d'ajouter Leanstral 1.5 à sa gamme expérimentale Labs, un modèle explicitement dédié à l'écriture et à la vérification de preuves formelles en Lean 4, le langage utilisé aussi bien par les mathématiciens que par les équipes de vérification logicielle.

Selon la documentation de Mistral, le modèle repose sur une architecture mixture-of-experts de 119 milliards de paramètres au total, dont 6,5 milliards seulement sont actifs par token. Le contexte monte à 256k tokens, et la fiche technique liste le function calling, le fill-in-the-middle, les sorties structurées et les agents. Publication le 30 juin 2026, tarif affiché à zéro, mise à disposition via l'API Mistral et la console Studio.

Pour comprendre l'intérêt du positionnement, il faut remonter à la version initiale sortie en mars 2026. D'après un article de Top AI Product, cette première Leanstral s'appuyait sur la base Mistral Small 4, activait 4 experts sur 128 par token, et avait été entraînée avec des capacités d'appel d'outils pour lean-lsp-mcp, le serveur MCP qui expose le langage Lean. Sur le benchmark FLTEval, elle atteignait 21,9 en pass@1 et 26,3 en pass@2, sous licence Apache 2.0.

Le point honnête à souligner, c'est que la fiche de Leanstral 1.5 ne publie aucun benchmark mis à jour et ne précise pas non plus la licence appliquée à cette révision. On sait qu'il s'agit d'un modèle updated, pas de combien. Le tarif nul est par ailleurs typique du statut Labs, un cadre expérimental dont la pérennité n'est pas garantie.

Pour les équipes qui vivent dans Lean 4, formalisation mathématique ou vérification de code, disposer d'un modèle spécialisé accessible gratuitement via API change quand même la donne côté outillage. Reste à voir si 1.5 tient la comparaison sur du vrai code, au-delà des scores FLTEval de la première mouture.