Leanstral 1.5, un nouveau modèle d'intelligence artificielle open source sous licence Apache 2.0, marque une avancée majeure dans le domaine de la vérification formelle et de la génération de preuves mathématiques. Développé spécifiquement pour l'environnement Lean 4, il se distingue par une architecture optimisée comptant 119 milliards de paramètres au total, dont six milliards sont actifs lors des calculs. Cette conception garantit des performances élevées tout en restant économe en ressources. Entraîné par une approche en trois étapes combinant pré-entraînement intermédiaire, ajustement fin supervisé et apprentissage par renforcement avec la méthode CISPO, le modèle atteint des résultats de pointe sur plusieurs benchmarks. Il résout la totalité des exercices du jeu miniF2F, complète 587 des 672 problèmes du PutnamBench, et établit de nouveaux records sur FATE-H et FATE-X. Grâce à sa capacité à étendre ses raisonnements sur plusieurs millions de jetons lors de l'exécution, Leanstral 1.5 résout des preuves complexes avec un coût estimé à quatre dollars par problème, loin derrière les centaines de dollars requis par ses concurrents directs. Au-delà des défis mathématiques, le modèle prouve son utilité dans la vérification de code réel et l'ingénierie logicielle. Dans des tests menés sur 57 dépôts open source, une chaîne d'automatisation intégrant Leanstral a identifié 11 vulnérabilités, dont cinq jamais signalées, démontrant sa capacité à détecter des erreurs que les tests classiques ou le fuzzing peuvent manquer. Il a également réussi à prouver formellement la complexité temporelle logarithmique d'une implémentation réelle d'arbres AVL, confirmant sa fiabilité pour des tâches de validation technique exigeantes. Disponible gratuitement sur Hugging Face et accessible via une API publique, Leanstral 1.5 s'adresse aux chercheurs et aux développeurs souhaitant intégrer des méthodes formelles dans leurs workflows quotidiens. Son déploiement est simplifié via l'environnement Mistral Vibe et ses outils complémentaires. Cette release confirme que les techniques de vérification formelle, longtemps réservées à des contextes académiques très spécialisés, deviennent progressivement accessibles, pratiques et économiquement viables pour l'industrie logicielle.