📰 Mistral 发布 Leanstral：首个面向 Lean 4 的开源代码智能体，支持形式化证明

Mistral 发布了 Leanstral，这是首个专为 Lean 4（证明助手）设计的开源代码智能体。

• 仅需 60 亿活跃参数即可高效运行，远低于同类模型
• 支持 MCP 协议，可通过 vibe 扩展功能
• 在 FLT 项目形式化证明测试中，单次通过即可超越 GLM5 和 Kimi-K2.5 等更大模型
• 运行成本仅 36 美元（pass@2），约为 Claude Sonnet 的 1/15
• 已开源 Apache 2.0 权重，可本地部署

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

🕐 发布于: 2026年03月17日 18:04