La empresa francesa Mistral ha presentado Leanstral 1.5, un modelo de inteligencia artificial con licencia Apache 2.0 orientado a la ingeniería de demostraciones formales en el lenguaje Lean 4. El sistema, con 119.000 millones de parámetros totales y solo 6.000 millones activos, alcanza resultados de referencia en varias pruebas de razonamiento matemático: satura la evaluación miniF2F con el 100 % de acierto, resuelve 587 de los 672 problemas de PutnamBench y registra un nuevo máximo del 87 % en FATE-H y del 34 % en FATE-X.
El modelo se entrena en tres etapas —preentrenamiento, ajuste supervisado y aprendizaje por refuerzo con el algoritmo CISPO— y combina un entorno multiturno con otro tipo agente de código, en el que edita archivos, ejecuta comandos y consulta el servidor de lenguaje de Lean en tiempo real. Según Mistral, Leanstral 1.5 muestra la curva de escalado en tiempo de prueba más sólida observada hasta ahora en modelos de razonamiento formal: en PutnamBench pasa de 44 problemas resueltos con 50.000 tokens a 587 con 4 millones, con un coste aproximado de 4 dólares por problema frente a los más de 300 de su rival Seed-Prover 1.5.
Además de los resultados en matemáticas, Mistral publica dos casos prácticos de verificación de código: una demostración completa de la complejidad logarítmica de los árboles AVL, lograda tras 2,7 millones de tokens y 22 compactaciones de contexto, y un proceso automatizado que, aplicado a 57 repositorios, identificó 47 propiedades violadas, 11 de ellas correspondientes a errores reales, 5 inéditos en GitHub. La compañía también ha liberado FLTEval, un banco de pruebas basado en pull requests reales del repositorio del último teorema de Fermat, y ofrece los pesos del modelo en Hugging Face y un punto de acceso gratuito a través de su API.