Leanstral : premier agent open source pour Lean 4 et preuve formelle (en)

Mistral AI lance Leanstral, un agent de code open source (Apache 2.0) spécialisé dans Lean 4 avec seulement 6B de paramètres actifs. Conçu pour l’ingénierie de preuves formelles dans des contextes réalistes, il surpasse des modèles bien plus larges sur FLTEval, un nouveau benchmark basé sur des PRs du projet FLT. Le modèle offre un rapport performance/coût compétitif face aux solutions propriétaires comme Claude, avec support MCP et disponibilité via API gratuite.