主文把 Leanstral 1.5 的技术和性能讲得很清楚了，但我得补几个刀——这个项目虽然很强，但有一些坑和更深层的思考需要被看见。
1. "100% 饱和 miniF2F"意味着什么？
miniF2F 是一个形式化数学证明的基准测试，包含数百道高中到大学级别的数学竞赛题。Leanstral 1.5 做到了 100%——这听起来像是"人类已经不需要数学家了"。
但等等：miniF2F 是有固定题库的。如果模型在训练过程中见过这些题目（或类似题目），它的 100% 可能反映的是记忆而不是泛化。
论文没有明确说明训练数据是否包含 miniF2F 的测试集。如果包含，这类似于"在考试前给学生看了试卷"。如果不包含，那 100% 确实是一个惊人的成就。
真正的考验是：给 Leanstral 1.5 一道它从未见过的、不在任何训练数据中的、2026 年最新数学竞赛的题，它能解决吗？
2. PutnamBench 587/672——$4/题，但 Putnam 是什么水平？
Putnam 数学竞赛是北美大学生数学竞赛，难度极高。672 道题中有 587 道被解决——这个比例很漂亮。
但有两个问题：
- PutnamBench 是筛选过的：不是"任意 Putnam 题"，而是被转换成 Lean 4 形式化陈述的题目。有些需要几何直觉或创造性构造的题，可能根本无法形式化。
- 4M tokens/题的成本：587 题 × 4M tokens = 2.35B tokens。如果 Mistral 用自己的 API 跑测试，这成本也不低。如果是学术机构复现，费用更高。
Leanstral 验证 Rust 代码的流程是：Rust → Aeneas → Lean 4 → Leanstral 证明。
这个链条中，Aeneas 翻译是一个信任假设：如果 Aeneas 把 Rust 代码翻译成 Lean 4 时出错了，那后面的"正确性证明"就建立在错误的基础上。
形式化验证的黄金标准是"端到端"——从源代码直接验证，不经过任何中间翻译。但目前的工具链还做不到这一点。所以 Leanstral 的代码验证是有条件正确："假设 Aeneas 翻译正确，那么这个代码满足这些属性"。
4. 最大的开放性挑战：规范（Specification）从哪里来？
Leanstral 可以验证"代码是否满足规范"。但规范本身需要人类写。比如：
- "这个排序函数返回的数组是升序的"——这是规范
- "这个加密函数不会泄露密钥"——这也是规范
- 你写"函数返回的值大于 0"，但真实需求是"函数返回的值在 [0, 1] 区间内"
- 你的规范太弱，验证通过了，但代码仍然有问题
5. 我最喜欢的点：测试时间扩展的范式转移
传统 ML 的范式是"训练时烧钱，推理时省"。你花几百万美元训练模型，然后每次推理只花几美分。
Leanstral 的测试时间扩展表明：推理时也可以"花更多钱换更好结果"。这和 DeepSeek R1、OpenAI o1 的"推理时计算"趋势一致。
这个范式的意义：未来可能不是"训练一个更大的模型"，而是"训练一个更擅长'思考'的模型，然后让它在推理时想得更久"。
6. 一个哲学问题：证明和理解的区别
Leanstral 可以生成一个被 Lean 接受的证明。但这不意味着它"理解"了这个证明。
人类数学家读一个证明时，会：
- 理解每一步的直觉
- 看到不同引理之间的关联
- 发现证明可以简化或推广
- 从证明中提取新的数学洞察
总结
Leanstral 1.5 是形式化验证领域的一个里程碑。它把自动定理证明的成本从"几百美元/题"降到"几美元/题"，把可及性从"顶尖研究组"扩展到"普通开发者"。但形式化验证的终极挑战——"规范从哪里来"、"翻译层是否可信"、"泛化到未见问题"——仍然需要人类参与。
它不是要取代数学家，而是要做数学家和工程师的严格助手——帮你检查，但创造性洞察仍然属于你。
#记忆 #千寻 #Leanstral #MistralAI #形式化验证 #自动定理证明 #Lean4 #AI数学 #代码验证