Mistral ha lanzado Leanstral 1.5, un modelo especializado en demostrar teoremas matemáticos en Lean 4, y lo ofrece gratis en su nivel Labs, según su ficha técnica. La diferencia con un modelo de propósito general es que aquí la salida no se queda en plausible: Lean 4 verifica cada paso, así que lo que el modelo propone está probado o no pasa.
Puntos clave
- Arquitectura Mixture-of-Experts: 119.000 millones de parámetros totales, 6.500 millones activos.
- Ventana de contexto de 256.000 tokens.
- Especializado en pruebas formales en Lean 4: demostración de teoremas y autoformalización.
- Soporta chat completions, function calling, structured outputs y Fill-in-the-Middle.
- Gratis (0 dólares) en el nivel Labs de Mistral.
- Sucede al Leanstral de marzo de 2026, ya discontinuado.
Qué hace y cómo funciona
Leanstral 1.5 tiene dos trabajos. Uno es demostrar teoremas: le das un objetivo matemático y propone los pasos de la prueba. El otro es autoformalización, que consiste en traducir un enunciado escrito en lenguaje natural a Lean 4, el lenguaje formal en el que se puede verificar. Un ejemplo para aterrizarlo: escribes en español "la suma de dos números pares siempre es par", y el modelo lo convierte en el enunciado formal de Lean 4 que una máquina puede comprobar sin ambigüedad. Ese paso de la frase de andar por casa al lenguaje formal es lo que se llama autoformalizar, y es el que suele atascar a quien no domina Lean.
El bucle es lo interesante. El usuario da el objetivo, el modelo propone los pasos, y Lean 4 los comprueba uno a uno. Si un paso no cuadra, no cuela. No hay margen para una respuesta que suene bien pero esté mal, porque el verificador la rechaza.
Por qué la arquitectura importa para el coste
Por dentro usa una arquitectura Mixture-of-Experts, que en cristiano funciona así. En vez de un solo cerebro gigante que se activa entero para cada pregunta, el modelo se divide en muchos "expertos" pequeños, y para cada consulta solo despierta a los que hacen falta. Por eso las cifras: 119.000 millones de parámetros totales, pero solo 6.500 millones activos en cada consulta. Tienes el conocimiento de un modelo enorme, pero pagas cómputo como si fuera uno mucho más pequeño. Y ahí está la clave del precio: mover 6.500 millones de parámetros por consulta cuesta una fracción de mover 119.000 millones, y eso es lo que permite ofrecerlo gratis sin arruinarse en servidores. La ventana de contexto es de 256.000 tokens, espacio de sobra para pruebas largas con muchos pasos y definiciones previas.
Qué trae para desarrolladores
Más allá de las matemáticas, Leanstral 1.5 soporta las funciones que un desarrollador espera: chat completions, function calling, structured outputs y Fill-in-the-Middle, es decir, completar código a partir del hueco y no solo del final. Sucede al primer Leanstral, que Mistral sacó en marzo de 2026 y ya ha discontinuado, así que este es el modelo vivo de la línea. La parte que baja la barrera es el precio: 0 dólares en el nivel Labs de Mistral. Un modelo gratis para un nicho tan concreto invita a que investigadores y equipos lo prueben sin justificar un presupuesto.
Por qué importa
El titular no es "otro modelo de IA". Es la idea de IA verificable. En lugar de fiarte de que la salida suene correcta, una máquina comprueba que lo es. Y aquí está el puente con el código que sí usas: cuando le pides a una IA que te escriba una función, hoy la lees y cruzas los dedos, porque puede compilar y aun así estar mal. La verificación formal apunta a otra cosa, a acoplar el modelo a un comprobador que diga sí o no sobre si el código hace lo que promete, sin opinar. Ese principio, verificar en vez de confiar, es justo lo que hace falta para usar IA en código serio, donde un error plausible cuesta caro. Para un directivo, el caso concreto de teoremas en Lean 4 es un nicho de investigación, no algo que vayas a meter en tu empresa mañana. Pero la dirección importa. La pregunta que todos nos hacemos con la IA generativa es cómo confiar en una salida que a veces se inventa cosas. La respuesta que apunta aquí es acoplar el modelo a un verificador. Cuando eso se lleve a la generación de código de producción, cambia el juego. Que Mistral lo ofrezca gratis ayuda a que se investigue más rápido.
Relacionado
