Mistral 发布开源代码智能体 Leanstral，面向 Lean 4 形式化证明

Mistral 发布 Leanstral，称其为首个面向 Lean 4 的开源代码智能体，权重采用 Apache 2.0 许可证，提供 120B-A6B 稀疏架构（6B 激活参数），并集成于 Mistral Vibe 及免费 API 端点 labs-leanstral-2603。