NEAR AI 团队用 DeepSeek V4 以约 111 美元成本解出 PutnamBench 全部 672 道数学题，推动链上代码形式化验证低成本化

NEAR AI 团队调用开源模型 DeepSeek V4，以总计约 111.85 美元的成本解出 PutnamBench 基准测试中的全部 672 道数学难题，平均每题仅 0.17 美元。该方案生成的 Lean 4 证明代码可被机器完全验证，其单题成本约为 GPT-5.6 的二百五十分之一。目前相关代码已开源，NEAR 计划将此低成本工具应用于协议及智能合约的形式化验证，旨在降低链上安全审计门槛。