，据NEAR Protocol联合创始人Alex Skidanov及官方披露，NEAR AI的Agent已解出PutnamBench全部672道数学题，总花费约111.85美元，平均单题0.17美元。该基准将北美顶级本科数学竞赛（William Lowell Putnam）题目形式化，要求以Lean 4证明助手语言写出无语法漏洞、可被机器100%验证的证明代码，对应计算机科学中的形式化验证，即用数学逻辑证明智能合约在所有可能状态下不出错。据MSBIntel整理的数据，使用OpenAI GPT-5.6的单题