Mistral发布Leanstral 1.5：Apache开源Lean 4代码智能体模型
sophiamyang · x · 2026-07-04
Mistral AI发布Leanstral 1.5，这是一个基于Apache-2.0协议的开源Lean 4代码智能体模型。在PutnamBench数学竞赛基准测试中，该模型成功解决672道题中的587道，展现出卓越的形式化数学证明能力。这是面向数学定理证明与形式化验证场景的专业化AI模型，代表Mistral在数学推理领域的重要进展。
所属事件:Mistral发布开源Lean 4证明智能体Leanstral 1.5(5 条相关)→
「编程与Agent」频道最新
- Fable 5.1 生成 three.js 网站实测：快且精准，但细节仍需人把关 — repligate · 2026-09-03
- SentinelX 开源：让 LLM 安全接管你的 Linux 服务器终端 — CarolusX74 · 2026-09-03
- 连载 30 天：用 fable 5.1 给户外机器人写出无线手柄控制器 — _Stocko_ · 2026-09-03
- 试水 AmpCode：可用 ChatGPT 订阅、每线程一台云电脑，槽点是吉祥物 Puck — carlosdponx · 2026-09-03
- 一人一 Agent 独立 microVM:语言学习产品上线生产环境的三个教训 — maritime_sh · 2026-09-03
- 断网手写 10 页文档后让 Agent 做成 PPT：作者发现自己文字像 AI 糊弄产物 — cnakazawa · 2026-09-03