Mistral发布开源代码助手Leanstral，专为Lean4证明辅助系统设计。该工具能在执行任务时严格验证代码实现，解决高风险领域人工审核瓶颈问题。相比现有系统，Leanstral更高效（6B参数），专注于实际形式化代码库操作，推动可信代码生成发展。

标题：Leanstral：开源可信代码生成的基础框架

来源：Mistral AI 官网 发布时间：2026年3月16日

核心内容：

随着AI代码生成工具在关键领域（如前沿数学研究和关键任务软件开发）的应用，人工审核成为制约工程效率的主要瓶颈。为此，Mistral AI推出首款专为Lean 4设计的开源代码代理Leanstral，它能执行任务并严格验证实现方案。

产品亮点： 1. 开放获取：采用Apache 2.0许可证，提供模型权重、Mistral Vibe集成和免费API 2. 高效架构：仅60亿活跃参数，专为实际形式化代码库优化 3. 可升级性：支持通过vibe进行任意MCP升级

性能表现： - 在FLT项目PR测试中，Leanstral-120B-A6B以单次推理超越GLM5-744B（16.6分）和Kimi-K2.5-1T（20.1分） - 对比Claude系列：Leanstral pass@2得分26.3，成本仅36美元，性价比显著优于Sonnet（549美元/23.7分）

实际案例： 1. 成功诊断Lean 4.29.0-rc6版本中类型别名导致的编译问题，提出将"def"改为"abbrev"的解决方案 2. 准确转换Rocq语言程序到Lean，并实现自定义符号和属性证明

使用方式： - 通过Mistral Vibe即时体验（指令/leanstall） - 免费API端点（labs-leanstral-2603） - 支持本地部署（Apache 2.0授权模型）

（注：原文中的性能对比表格、数学概念示例等细节已精简，保留核心数据点和典型应用场景）

以下是评论内容的总结：

1. 积极评价

   • 对Mistral团队表示祝贺，期待更多基准测试结果
     "This is great, congratulations to the Mistral team! I'm looking forward to the code arena benchmark results."
     "Truly exciting"

2. 性能与成本讨论

   • 认为虽然成本更低，但性能差距明显，Opus可能更值得
     "Opus costs about 6x more...totally worth it based on the task at hand."
     "Haiku kinda sucks at this task...why would 'yeah it sucks but it's 10 times cheaper' be relevant?"
   • 有用户提出通过多模型组合可能提升性能
     "would performance increase if they used different models per pass"

3. 技术细节疑问

   • 对"passes"概念和比较基准提出疑问
     "What are these 'passes' they reference here?"
     "Does Mistral come close to Opus 4.6 with any of their models?"

4. 负面评价

   • 个别用户对公司存续表示质疑
     "No idea how this company is still in business."

5. 实际应用案例

   • 引用实际成功案例说明模型价值
     "The model correctly identified that because def creates a rigid definition..."