📰 Mistral发布Leanstral：可信vibe-coding的开源基础

Mistral发布Leanstral，这是首个专为Lean 4设计的开源代码代理，可用于形式化证明和严格规范验证。

• 高效设计：仅需60亿活跃参数，通过Lean作为完美验证器实现并行推理
• 性能领先：pass@2得分26.3，超越Sonnet 2.6分，成本仅需6（对比Sonnet的49）
• 开源可用：权重采用Apache 2.0许可证发布，可通过Mistral vibe和免费API调用
• 支持MCP：通过vibe支持任意MCP，尤其是针对lean-lsp-mcp进行了专门训练
• 评估突破：发布FLTEval新评估套件，专注于实际形式化工程任务而非竞赛数学

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

🕐 发布于: 2026年03月17日 08:03