Ce que Mistral a ouvert

Le 2 juillet 2026, le laboratoire français d'IA Mistral a publié Leanstral 1.5 sous licence Apache-2.0, avec des poids ouverts sur Hugging Face et un point d'accès API gratuit. D'après l'annonce même de Mistral, c'est un modèle à mélange d'experts, 119B de paramètres au total dont environ 6B actifs et un contexte de 256k jetons, spécialisé dans la démonstration formelle de théorèmes en Lean 4 et l'autoformalisation. En clair, prouver en Lean 4 revient à transformer une affirmation sur votre logiciel en un énoncé qu'une machine vérifie ligne à ligne, de sorte que la correction est démontrée et non supposée.

Les résultats des tests de référence frôlent la saturation : 100 pour cent sur les jeux de validation et de test miniF2F, 587 problèmes PutnamBench résolus sur 672, 87 pour cent sur FATE-H et 34 pour cent sur FATE-X, avec un fort passage à l'échelle au calcul, de 44 problèmes à petit budget jusqu'à 587 à grand budget. Plus parlant pour un dirigeant, lors des tests le modèle a mis au jour 5 bugs jusque-là inconnus dans 57 dépôts de code, dont un débordement critique dans une bibliothèque de décodage zigzag que les tests classiques laissent d'ordinaire passer. Champion national français, Mistral place ici la souveraineté numérique au coeur de l'ouverture.

Écrire le code était la moitié facile

Faire écrire du code par une IA est en grande partie résolu. Prouver que ce code est correct ne l'est pas, et c'est la moitié qui compte pour tout ce que vous ne pouvez pas vous permettre de rater. À mesure que les modèles produisent davantage de votre logiciel, le volume de code dépasse la capacité humaine de relecture, et la couche de vérification devient en silence le goulot d'étranglement et la vraie garantie.

Voilà pourquoi un moteur de preuve comme Leanstral pèse plus qu'un énième générateur de code. Pour le logiciel critique et réglementé, la correction prouvable passe du luxe académique à un critère réaliste d'appel d'offres, où une preuve démontrée vaut ce qu'aucune suite de tests réussis n'égale. Le dirigeant qui peut attester qu'un composant est prouvé, et pas seulement testé, négocie d'une position plus solide face aux régulateurs, aux assureurs et aux clients.

Posséder le vérificateur

Le sujet de souveraineté n'est pas ici un énième agent conversationnel. C'est le vérificateur. Parce que Leanstral est livré en poids ouverts européens sous Apache-2.0, vous pouvez exécuter la couche de vérification en interne, inspecter exactement ce qu'elle fait et la conserver, plutôt que d'appeler une API américaine et de vous fier à une boîte noire que vous ne voyez ni ne gardez.

Ainsi la couche de confiance de votre chaîne d'approvisionnement logicielle reste auditable et sous votre contrôle. Quand les machines écrivent le code, la question décisive est de savoir à qui appartient la machine qui vérifie la machine. Un moteur de preuve que vous exécutez vous-même répond à cette question en votre faveur, sans vous obliger à céder votre code le plus sensible à un service extérieur.

À lire ensuite: Votre renouvellement Microsoft est un levier  ·  Le cloud souverain a desormais une note