NEAR AI 仅花费111美元解出672道 PutnamBench 题目，成本仅为原来的1/250

NEAR AI 仅花费 111 美元就解决了 PutnamBench 数学基准测试中的全部 672 道题，成本仅为已知第二低成本提交的 1/250。NEAR Protocol 联合创始人 Alex Skidanov 于 2026 年 9 月 6 日宣布了这一结果，并强调开源 Lean 智能体在完成这套取自 William Lowell Putnam 数学竞赛的题目时展现出的效率。这一突破解决了此前的成本壁垒：完整运行基准测试每次需要投入 1 万至 2.5 万美元，只有具备相应资金实力的组织才能承担，而 NEAR AI 则将这项成就置于其面向机密且可验证 AI 系统的 IronClaw 框架之中。

PutnamBench 基准测试使用 Lean 4 证明助手处理 672 道题

Putnam 竞赛是北美最负盛名的本科数学竞赛，即使是成绩优异的学生也常常得零分。PutnamBench 于 2024 年推出，将这种难度转化为面向 AI 定理证明器的正式评估套件。该基准测试包含 672 道使用 Lean 4 编码的问题。Lean 4 是一种证明助手语言，要求以机器可验证的精确性书写数学论证。逻辑不完整的证明会被直接判定为无效，不会获得部分分数。

在 NEAR AI 取得这一结果之前，尝试 PutnamBench 的智能体通常每道题需要数千次推理调用。计算成本迅速累积，使先进系统完整运行基准测试的支出达到 1 万至 2.5 万美元。NEAR AI 的 Lean 智能体仅花费 111 美元就完成了全部 672 道题。

NEAR AI 实现 111 美元总成本，远低于行业 1 万至 2.5 万美元的成本范围

在每次完整运行需花费 1 万至 2.5 万美元的情况下，只有少数组织能够负担得起定理证明流程的迭代与改进。成本降至 111 美元后，这一限制实际上已被消除。2025 年至 2026 年间 PutnamBench 成绩的快速提升，源于将大型语言模型与 Lean 证明检查引擎相结合的智能体工作流。NEAR AI 的方法延续了这一模式，同时实现了基准测试社区此前未曾观察到的效率水平。

NEAR AI 将这项成就置于以 IronClaw 为核心的更广泛基础设施愿景之中，该框架致力于构建机密且可验证的 AI。形式化验证能力与这一定位直接契合：在机器层面证明数学论证的正确性，为 AI 系统奠定了基础，使其输出能够被独立审计，而不是依赖主观信任。

NEAR AI 将 Lean 智能体作为开源工具发布

NEAR Protocol 将 Lean 智能体开源。能够带来 250 倍成本优势的专有工具通常会继续保持专有。将该智能体开源后，任何一方都可以检查、扩展和使用其方法。此举消除了研究人员和组织获取相关技术的障碍，使其能够复现或进一步构建 PutnamBench 结果中展示的高效技术。

常见问题

NEAR AI 于 2026 年 9 月 6 日取得了什么成就？
正如 NEAR Protocol 联合创始人 Alex Skidanov 所宣布的那样，NEAR AI 的开源 Lean 智能体以 111 美元的总成本解决了 PutnamBench 基准测试中的全部 672 道题。已知成本第二低的提交所需成本是其 250 倍。

为什么 111 美元的成本对 PutnamBench 很重要？
此前，完整运行基准测试的成本为 1 万至 2.5 万美元，除资金充足的组织外，其他参与者很难承担。在 111 美元的成本下，定理证明系统迭代和实验的成本壁垒实际上已被消除。

什么是 PutnamBench，它如何运作？
PutnamBench 是一套于 2024 年推出的评估套件，包含 William Lowell Putnam 数学竞赛中的 672 道题，并使用 Lean 4 证明助手编码。该基准测试要求提供机器可验证的数学证明，逻辑不完整的证明不会获得部分分数。