Mistral做了个证明机器，还比Opus便宜

Mistral刚发了Leanstral 1.5，有个数字得先记住：672道题里做出587道。这是PutnamBench，普特南竞赛数学，大部分模型碰都碰不动，它做出来587道。miniF2F直接100分打满，FATE-H和FATE-X都是SOTA，真实的证明工程任务上，它比Claude Opus 4.6还强，成本却低一大截。全开源，Apache-2.0，Hugging Face上能下，还给免费API。

这东西说白了是个119B的MoE模型，每次只激活6B参数，专门干一件事——用Lean 4写形式化证明。不是那种嘴上说说的数学，是真正过编译器的机器可验证证明。编译器要么认，要么不认，没有含糊空间，也没有那种看着对其实是瞎编的引理。证明能通过类型检查就是过，不过就是不过。

比数学更值得看的是这一段：它在真实开源仓库里挖出5个之前没人报过的bug，还证明了AVL树的时间复杂度保证。形式化验证以前是博士生的全职工作，现在你把它对准一个代码库，它就开始证明你的代码是对的——或者告诉你哪里不对。

真正暴露它走向的是test-time scaling那条曲线。给5万token，做出44道普特南题；给到400万token，做出587道。算力越多，证明越多，几乎是线性的。这就是那种你晚上甩给它一块GPU预算，第二天早上醒来代码库已经被验证过一遍的工具。

链接：mistral.ai/news/leanstral-1-5