Leanstral, l'agent de code open source de Mistral pour Lean 4

Leanstral, publié par Mistral AI, est présenté comme le premier agent de code open source conçu pour Lean 4, un assistant de preuve capable de formaliser aussi bien des objets mathématiques complexes que des spécifications logicielles. L'idée de fond : plutôt que de faire relire par un humain du code généré par IA, goulot d'étranglement dès que les enjeux montent, l'agent prouve formellement que son implémentation respecte une spécification stricte. L'humain dit ce qu'il veut, la machine le démontre.

Là où d'autres systèmes de preuve enveloppent de gros modèles généralistes ou se limitent à des problèmes isolés, Leanstral mise sur l'efficacité, avec une architecture très parcimonieuse à 6 milliards de paramètres actifs, et sur l'entraînement dans des dépôts formels réalistes. Il s'appuie sur Lean comme vérificateur et gère les MCP via l'environnement Mistral Vibe. Selon Mistral, il rivalise avec des modèles bien plus volumineux tout en coûtant nettement moins cher.

Les poids sont diffusés sous licence Apache 2.0, et le modèle est accessible dès maintenant dans Mistral Vibe, via un point d'accès API gratuit, ou en téléchargement pour tourner sur sa propre infrastructure. Mistral y ajoute un rapport technique et une nouvelle suite d'évaluation, FLTEval.