Mistral 发布开源代码智能体 Leanstral，专为 Lean 4 形式化证明设计

Mistral 发布首个面向 Lean 4 的开源代码智能体 Leanstral-120B-A6B（6B 激活参数），权重采用 Apache 2.0 许可，可通过 Mistral Vibe 和 labs-leanstral-2603 免费 API 端点使用。