Mistral lanza Leanstral: el primer agente de código de código abierto para Lean4, que genera código y produce pruebas formales simultáneamente

Según la información de Binance News, según la monitorización de 1M AI News, Mistral AI lanzó hoy Leanstral, el primer agente de código abierto diseñado específicamente para la herramienta de verificación formal Lean 4. El núcleo de la generación de código por IA es la revisión manual, pero Leanstral permite que la IA genere código junto con pruebas formales verificables automáticamente por Lean 4, evitando esa etapa. El modelo utiliza una arquitectura sparse MoE, con 120 mil millones de parámetros totales y 6 mil millones de parámetros activos, de código abierto bajo Apache 2.0, y ha sido optimizado específicamente para lean-lsp-mcp. Puede iniciarse sin configuración en Mistral Vibe (comando /leanstall) o mediante la API gratuita en el endpoint labs-leanstral-2603, soportando la descarga y auto-despliegue de pesos. Mistral también lanzó la nueva evaluación FLTEval, basada en el proyecto formal del teorema de Fermat en la comunidad Lean 4. En comparación de costos: Leanstral pass@2 obtiene una puntuación de 26.3 con $36, superando a Claude Sonnet 4.6 con $549 y una puntuación de 23.7; en pass@16, con $290, obtiene 31.9 puntos, 8 puntos por delante de Sonnet 8, mientras que Claude Opus 4.6 necesita $1,650 para alcanzar 39.6 puntos. Entre los modelos de código abierto, Qwen3.5-397B-A17B requiere 4 ejecuciones para llegar a 25.4 puntos, aún por debajo de Leanstral pass@2.