Labs Leanstral 1 5

Le 16 mars 2026, Mistral AI a franchi une étape majeure dans le domaine de l'intelligence artificielle appliquée aux sciences exactes en annonçant Leanstral. Présenté comme son premier agent de code open source conçu spécifiquement pour Lean 4, ce modèle vise à résoudre un goulot d'étranglement critique : la revue humaine dans les domaines à forts enjeux, tels que la recherche mathématique et le développement de logiciels critiques.

Bien que certaines configurations fassent référence à l'identifiant labs-leanstral-1-5, les documentations officielles et la fiche Hugging Face répertorient ce modèle sous l'identifiant labs-leanstral-2603 (ou Leanstral 26.03). Ce modèle marque une rupture avec les générateurs de code généralistes en se focalisant sur la production de preuves formelles vérifiables par machine.

Architecture et caractéristiques techniques

Leanstral 26.03 est un modèle issu de la famille Mistral Small 4, distribué sous licence open source Apache 2.0. Sur le plan architectural, il s'agit d'un modèle à mélange d'experts (MoE) particulièrement sophistiqué : - Paramètres totaux : 119 milliards de paramètres. - Paramètres actifs : 6,5 milliards de paramètres par token. - Structure MoE : 128 experts au total, dont 4 sont activés pour chaque token.

En termes de modalités, Leanstral accepte des entrées multimodales (texte et image) mais produit exclusivement des sorties textuelles. Il n'intègre aucune capacité native de génération d'images, d'audio ou de synthèse vocale, concentrant toute sa puissance sur le traitement symbolique et textuel.

La fenêtre de contexte officielle s'élève à 256 000 tokens. Toutefois, pour des performances optimales en situation réelle, les recommandations techniques préconisent de limiter les requêtes à un contexte inférieur ou égal à 200 000 tokens, en configurant une température de 1.0 et un niveau d'effort de raisonnement élevé (reasoning_effort="high") pour les tâches de preuve complexes. Bien que l'API n'affiche pas de limite de sortie contractuelle stricte, les implémentations locales documentées utilisent couramment une configuration à 32 000 tokens de sortie.

Positionnement et performances comparatives

Pour évaluer Leanstral, Mistral AI a privilégié le benchmark FLTEval, un protocole orienté vers la preuve Lean 4 au sein de pull requests réelles, notamment liées au projet de formalisation du dernier théorème de Fermat. Ce choix méthodologique s'écarte des évaluations sur problèmes mathématiques isolés pour se confronter à l'ingénierie de preuve en conditions réelles.

Selon les données fournies par l'éditeur : - Face aux modèles open source géants : Leanstral (120B-A6B) surpasse des architectures nettement plus massives telles que GLM5-744B-A40B et Kimi-K2.5-1T-A32B. De même, face à Qwen3.5-397B-A17B (qui atteint un score de 25,4 avec 4 passes), Leanstral obtient un score de 26,3 dès le protocole pass@2. - Face aux modèles propriétaires de référence : Dans le protocole de test de Mistral, Leanstral (pass@2 à 26,3) s'avère extrêmement compétitif face à Claude Sonnet 4.6 (score de 23,7). L'argument économique est ici massif, le coût estimé pour le protocole s'élevant à 36 $ pour Leanstral contre 549 $ pour Claude Sonnet 4.6. Bien que Claude Opus 4.6 conserve l'avantage en termes de performance brute avec un score de 39,6, son coût d'exécution s'envole à 1 650 $ dans ce même protocole.

Note : Ces mesures émanent directement des benchmarks de l'éditeur et n'ont pas fait l'objet d'une validation indépendante systématique.

Cas d'usage et limites du modèle

Leanstral s'adresse en priorité aux ingénieurs de preuve, aux chercheurs en mathématiques et aux développeurs de systèmes critiques. Ses principaux cas d'usage incluent : - La formalisation de théories mathématiques et de spécifications logicielles en Lean 4. - La complétion automatique et interactive de preuves formelles. - La migration de bases de code existantes vers Lean 4. - La traduction de fragments de code d'autres assistants de preuve (comme Rocq) vers Lean. - L'analyse et le raisonnement logique sur des programmes complexes.

Néanmoins, plusieurs limites doivent être prises en compte. Sa spécialisation extrême sur Lean 4 le rend moins adapté aux tâches de développement généralistes. De plus, son statut de modèle "Labs" implique une disponibilité potentiellement transitoire. Mistral AI a d'ailleurs mentionné une date de dépréciation au 22 mai 2026 pour certaines versions de test, ce qui invite à la prudence quant à la pérennité de l'accès à long terme.

Il est à noter que Mistral AI propose actuellement un accès gratuit temporaire à l'endpoint labs-leanstral-2603 afin de stimuler les retours d'expérience de la communauté scientifique, bien que cet accès gratuit soit sujet aux politiques de dépréciation de l'éditeur.