Mistral AI·· 2026-03-17精选AI 评分70
Mistral 发布开源 Lean 4 代码智能体 Leanstral
Leanstral: Open-Source foundation for trustworthy vibe-coding
AI 导读
Mistral 发布面向 Lean 4 的开源代码智能体 Leanstral，模型为 Leanstral-120B-A6B，采用高稀疏架构和 6B 激活参数，权重以 Apache 2.0 许可开放。
推荐理由
原文给出 Apache 2.0 权重、Mistral Vibe 与免费 API 入口，并用 FLTEval 展示其在 Lean 4 证明工程中的成本和性能位置。
来源：Mistral AI · mistral.ai