给AI一道研究生级别的数学题，它不能只给答案，还得写出能通过机器检查的证明。这就是ProofBench在做的事。

这个基准由Vals AI联合一批Lean 4专家打造，专门衡量形式化定理证明能力。每道题都配有一句自然语言的定理陈述，以及一份经过审核的Lean 4形式化版本。模型要做的，是产出一份能被Lean 4检查器接受的证明。

打开网易新闻 查看精彩图片

题目难度落在研究生或高年级本科水平，覆盖分析、代数、概率、数论和逻辑几个方向。榜单跑在一个不公开的100道题的私有切分上，模型以智能体方式工作，可以调用Mathlib搜索和代码执行工具，每道题最多允许40轮交互。

分数怎么算

数据来自Vals AI公开的ProofBench榜单。图表呈现的是证明成功率，也就是模型的Lean 4证明通过形式化检查器的题目占比。

评分是二元的，每道题要么过要么不过，没有部分分。榜单的标准误、推理强度设置、延迟和单次测试成本，都保留在数据导出里。

因为证明是由Lean 4编译器检查，而不是由某个裁判模型打分，所以分数反映的是经过验证的形式正确性。每个模型只出现一次，采用Vals AI选定的固定推理强度配置。

榜单里还有个特殊选手

榜单还收录了Harmonic的Aristotle定理证明系统。它运行在自己的测试框架里，数据被存储下来，但没有进入图表排名。

形式化验证的好处在于，它把"证明对不对"这件事从主观判断变成了编译器的确定性输出。没有裁判偏好，没有评分尺度争议，过就是过。

代价也很直接：二元评分意味着没有中间地带，一道题卡在最后一步和完全没思路，在分数上没有任何区别。