作者：长安，深潮 TechFlow

深潮导读： 672 道北美顶级大学生数学竞赛题，被 NEAR AI 团队用 Agent 全部解出。总计花费约 111 美元，平均每题 0.17 美元。NEAR AI 团队调用中国开源模型 DeepSeek V4 完成了这次测试。这并非单纯的大模型智力竞赛，在算力账单背后，是一门试图将昂贵的智能合约“形式化验证”平民化的基建生意。

一份开源代码库的测试数据，把大模型解题的成本底牌翻了出来。

最近，根据 NEAR Protocol 联合创始人 Alex Skidanov 及官方侧公布的数据，NEAR AI 的 Agent 解决了 PutnamBench 上的全部 672 道数学难题。

给不熟悉的读者科普一下，PutnamBench 并非普通的题库，它是将北美顶级本科数学竞赛（William Lowell Putnam）题目形式化而成的基准测试。

说人话就是，让 AI 做严密的数学逻辑推导，看看能否自主进行解题。完成全部解答，NEAR AI 花了约 111.85 美元。平均下来，每道题的成本是 0.17 美元。

作为对比，其他拿到满分的方案账单要昂贵得多。

根据 MSBIntel 整理的数据，使用 OpenAI 的 GPT-5.6，单题平均成本高达 44.5 美元；使用 Anthropic 的 Claude Opus 5，每题也需要 3.52 美元。

在这个特定测试中，NEAR 采用 DeepSeek V4 的方案，将成本压缩到了 GPT-5.6 的二百五十分之一。

公链做数学题，醉翁之意不在酒

公链团队花力气解数学题，指向的并非教育市场。

PutnamBench 测试的核心要求，是机器的可验证性：AI 生成的不能只是一段文字答案，而是必须用 Lean 4（一种主流的证明助手语言）写出严格的证明代码。

这些代码不能有语法漏洞，不能跳过推导步骤，必须被机器 100% 验证通过。同时，这在计算机科学领域对应着一项关键技术，即形式化验证。

而关联到加密行业，智能合约承载着数亿甚至上百亿美元的资金。传统的代码审计依赖人工寻找漏洞，而形式化验证则是用严密的数学逻辑，一行行证明代码在所有可能状态下都不会出错。

长期以来，形式化验证的致命缺点是贵且慢。它需要顶级的安全专家和漫长的周期，通常只有资金雄厚的头部项目才负担得起。

NEAR AI 的这次测试，证明了用开源 AI 模型批量生成可靠数学证明的可行性，更验证了它的低成本。

链上安全的平民化基建

把形式化验证的门槛打到几毛钱，这是 NEAR 正在布局的实际业务。

目前，这套打通了 DeepSeek 和 Lean 4 的代码已经完全开源。NEAR 官方公开的下一步方向，是直接将这套低成本工具应用于 NEAR 协议自身以及核心智能合约的安全验证上。

所以，你可以把它理解成这是一次技术下放，或者更通俗的说叫项目方在做事，和 AI 叙事相关。

如果开源 AI 能够稳定输出机器可验证的代码安全证明，意味着未来的普通开发者和小微项目团队，也可以在部署合约前，用几毛钱的成本跑一次形式化验证，降低了智能合约出问题的概率。

不过客观来说，这与 NEAR 代币的短期价格涨跌没有直接关联。但在公链生态的底层竞争中，用几十美分去排雷，远比耗资百万事后补救更具真实的商业价值。