Leanstral 1.5 开源：Lean 4 形式化证明模型
sophiamyang · x · 2026-07-04
Sophia Yang 发布 Leanstral 1.5，一个面向 Lean 4 形式化证明工程的 119B（6B 激活）开源模型。在 miniF2F 取得 100%、PutnamBench 587/672（约 $4/题）、FATE-H 87% 与 FATE-X 34% 创 SOTA，并在真实开源项目中发现 5 个此前未知的 bug。采用 Apache-2.0 许可，权重托管于 HuggingFace 并提供免费 API。
所属事件:Mistral发布开源Lean 4证明智能体Leanstral 1.5(5 条相关)→
「模型」频道最新
- 传 OpenAI 在 Astra 中使用 neuralese 循环变换器，新的 scaling 轴浮出水面 — imadade · 2026-09-03
- XBOW 团队拿下今年首个 Chrome 全链漏洞利用奖励 — moyix · 2026-09-03
- Gemini 3.8 Flash 的 Pareto 最优地位仅维持了 5 小时 18 分钟 — alejandroll10 · 2026-09-03
- 双 DGX Spark 实测：GLM-5.3-Flash 写作与视觉胜过 DeepSeek-V4-Flash — kuhunaxeyive · 2026-09-03
- Anthropic 商务智能体只建购物车交人工结账,被赞退款风控思路对 — HaktanSuren · 2026-09-03
- Qwen3.8 27B Q8 翻车:12 万 token 后发现根本没读计划,自行实现别的功能 — KingCpzombie · 2026-09-03