Mistral ha lanzado Leanstral 1.5, un modelo de IA gratuito y de código abierto que hace algo inusual: ayuda a demostrar la corrección de código y matemáticas. La mayoría de los asistentes de código generan código y esperan que funcione. Leanstral 1.5 trabaja dentro de Lean 4, un asistente de demostraciones, donde cada paso se verifica. Según Mistral, se lanzó el 30 de junio de 2026 bajo la licencia Apache-2.0. Esto es lo que es, las cifras que afirma Mistral y dónde encaja realmente. Para ver el panorama más amplio, consulta nuestra visión general de los mejores LLM para programar en 2026.
Qué es Leanstral 1.5
Según Mistral, Leanstral 1.5 es un modelo de agente de código creado para Lean 4. Lean 4 es un asistente de demostraciones. Puede expresar objetos matemáticos complejos y también especificaciones de software, como propiedades de fragmentos de código en Rust.
Mistral dice que el modelo funciona como un desarrollador en un sistema de archivos real. Edita archivos, ejecuta comandos bash y usa el servidor de lenguaje de Lean. Eso le permite asumir tareas largas: completar una demostración parcial en un repositorio, construir lemas auxiliares y avanzar a través de muchas rondas de contexto.
En cuanto a las cifras, Mistral describe un modelo de mezcla de expertos con 119.000 millones de parámetros totales y unos 6.500 millones activos por token. Tiene una ventana de contexto de 256k tokens. Está en Hugging Face como mistralai/Leanstral-1.5-119B-A6B, con una API gratuita. Si ejecutas modelos en local, nuestra guía del mejor LLM local para programar ofrece el contexto más amplio.
Qué significa la verificación formal para los desarrolladores
Esta es la parte que importa, así que aquí va con claridad. Las pruebas comprueban tu código con algunas entradas. La verificación formal demuestra que es correcto para todas las entradas, usando matemáticas. Un asistente de demostraciones como Lean 4 verifica cada paso lógico. Si la demostración pasa, es una garantía, no una muestra.
Ese poder tiene un coste. Escribir demostraciones formales a mano es lento y difícil, y por eso la mayoría del software nunca se verifica. La esperanza detrás de un modelo como Leanstral es hacer ese trabajo más rápido y más accesible. Está más cerca de una herramienta de revisión de código con IA para la corrección que de un chatbot.
Las cifras de benchmark
Mistral reporta resultados sólidos en los benchmarks. Trátalos como las cifras propias del proveedor hasta que otros las reproduzcan.
Según Mistral, Leanstral 1.5 satura miniF2F y resuelve 587 de 672 problemas de PutnamBench. Mistral también afirma resultados de vanguardia en FATE-H con un 87% y FATE-X con un 34%. En FLTEval, Mistral dice que pass@1 sube de 21,9 a 28,9, y pass@8 sube de 31,9 a 43,2.
Estos son benchmarks de demostraciones, no pruebas generales de programación. Una puntuación alta en PutnamBench significa que el modelo es bueno en matemáticas formales difíciles. No significa que vaya a escribir tu aplicación web. Interpreta las cifras por lo que miden.
Qué significa para ti
Para la mayoría de los desarrolladores, Leanstral 1.5 no es una herramienta de uso diario hoy. Es una herramienta especializada para Lean 4 y demostraciones formales. Si no escribes demostraciones, no cambiará tu flujo de trabajo esta semana.
Pero la dirección merece atención. Un modelo de código abierto orientado a la corrección demostrable es una apuesta distinta de la habitual carrera del autocompletado de código. Con el tiempo, una verificación formal más barata podría llegar a más del código que realmente lo necesita: criptografía, aeroespacial, finanzas y contratos inteligentes. Si las demostraciones asistidas por IA se vuelven buenas y baratas, lo "probado" podría ceder poco a poco el paso a lo "demostrado" para el código de mayor riesgo.
Las advertencias honestas
Dos advertencias mantienen esto con los pies en la tierra. Primera, las cifras de benchmark son afirmaciones propias de Mistral, publicadas con el lanzamiento. Son prometedoras, pero es la reproducción independiente lo que convierte una afirmación en un hecho. Segunda, esta es una herramienta especializada. Lean 4 tiene una curva de aprendizaje pronunciada, y la verificación formal sigue siendo un trabajo de nicho, no algo que haga la mayoría de los equipos.
La lectura honesta: Leanstral 1.5 es un paso real, gratuito y capaz para un problema difícil, publicado de forma abierta para que cualquiera pueda probarlo. Esa apertura es la parte más fuerte de la historia. Si la corrección demostrable importa en tu trabajo, merece un vistazo. Si no, mantén un ojo en el espacio y quédate con las herramientas de nuestra recopilación de mejores asistentes de código con IA.
