Mistral presenta Leanstral, un agente open-source pensado para reducir el cuello de botella humano en la verificación de código y pruebas formales. ¿Te imaginas generar código que además se verifica automáticamente contra especificaciones estrictas? Esa es la idea: que la prueba no sea un trámite manual interminable, sino parte del propio agente.
Qué es Leanstral
Leanstral es el primer agente open-source entrenado específicamente para Lean 4, el asistente de pruebas capaz de expresar objetos matemáticos complejos y especificaciones de software. A diferencia de enfoques que envuelven modelos generalistas, Leanstral se diseñó para ser eficiente: tiene alrededor de 6B de parámetros activos y una arquitectura esparsa optimizada para tareas de proof engineering.
¿Qué significa esto en la práctica? Que no se trata solo de generar conjeturas: Leanstral genera, prueba y verifica dentro del flujo de trabajo formal, usando a Lean como verificador perfecto.
