Mistral AI 发布 Leanstral，面向 Lean 4 的开源代码智能体

Mistral AI 发布 Leanstral，称其为面向 Lean 4 的开源代码智能体，用于在严格规格下生成并证明实现。Leanstral 采用高度稀疏架构，拥有 6B active parameters，权重以 Apache 2.0 许可发布，并集成到 Mistral Vibe、提供 labs-leanstral-2603 API endpoint。