Mistral 发布开源 Lean 4 代码智能体 Leanstral

Mistral AI 发布 Leanstral，这是面向 Lean 4 的开源代码智能体，采用 6B 活跃参数，并针对真实形式化代码仓库中的证明工程任务训练。权重以 Apache 2.0 许可开放，可通过 Mistral Vibe 和免费 API 使用；文中称 API 端点仅在有限时期内保持高可用。