Mistral 发布开源 Lean 4 证明智能体 Leanstral

Mistral 发布 Leanstral，称其为首个面向 Lean 4 的开源代码智能体，权重以 Apache 2.0 许可开放，采用 120B-A6B 稀疏架构，并可通过 Mistral Vibe 和 labs-leanstral-2603 API 端点使用。