Mistral 发布 Leanstral：面向 Lean 4 的开源代码智能体
Leanstral: Open-Source foundation for trustworthy vibe-coding
发生了什么
Mistral 发布 Leanstral，称其为首个面向 Lean 4 的开源代码智能体，采用 6B 激活参数的稀疏架构，权重以 Apache 2.0 许可开放，并接入 Mistral Vibe 与免费 API 端点 labs-leanstral-2603。
推荐理由
Mistral 开源面向 Lean 4 的代码智能体，给出与 Claude 系列和开源模型的成本与得分对比，可据此判断形式化验证路线的性价比。
继续阅读
最新日报 · 第 24 期NVIDIA 与 AI4Bharat 推出 Nemotron-pretraining-Indic-v1 及开放数据生成流水线正在热议
明早 08:00 把这样一份日报发到你邮箱
和上面这份一样：几件值得看的事。免费，点确认信之后才会开始发送，每封信都能一键退订。 看一份往期日报 · 2026-10-17