📰 Mistral发布Leanstral：首个用于形式化证明的开源代码Agent

Mistral AI发布了Leanstral，这是首个专为Lean 4证明助手设计的开源代码agent。

• 基于6B活跃参数的高效稀疏架构，专门针对证明工程任务优化
• 通过Lean作为完美验证器实现并行推理，性能和成本效益优异
• 在FLTEval基准测试中，pass@2得分26.3，超越Sonnet 2.6分，成本仅6（Sonnet为49）
• pass@16达到31.9分，超越Sonnet 8分，而Opus成本高达650（Leanstral的92倍）
• 提供免费API端点（labs-leanstral-2603）、Apache 2.0许可权重和Mistral Vibe集成
• 支持通过MCP扩展，可与lean-lsp-mcp配合使用

原文链接：https://mistral.ai/news/leanstral

🕐 发布于: 2026年03月17日 12:01