解決數學中最艱難的基準測試中的每個問題，通常需要耗費數萬美元。NEAR AI 僅用 111 美元就完成了。
2026年9月6日，NEAR Protocol共同創辦人Alex Skidanov宣布，該項目的開源Lean代理已解決PutnamBench基準測試中的全部672個問題，該基準測試取材自William Lowell Putnam數學競賽。總費用為$111，第二便宜的已知提交方案成本高出250倍。
PutnamBench 到底是什麼，以及它為何重要
普特南競賽是北美最具聲望的本科數學競賽。即使是在聰明的學生中，得零分也並不罕見。這項考試的設計就是要擊垮你。
PutnamBench 於 2024 年推出，將這種難度傳統轉化為一套正式的 AI 定理證明評估套件。該基準測試包含 672 個以 Lean 4 編碼的問題，Lean 4 是一種證明輔助語言，要求數學論證以機器可驗證的精確性撰寫。邏輯上鬆散的證明將被直接拒絕，不設部分分數。
在 NEAR AI 的結果出現之前，嘗試 PutnamBench 的代理通常每個問題需要數千次推理調用。計算成本迅速累積，使主要系統的完整基準測試運行總支出達到 10,000 至 25,000 美元。
NEAR AI 的 Lean 代理以 111 美元完成了全部 672 個問題集。
為何成本差距才是真正的重點
每完整運行成本為 10,000 至 25,000 美元時，僅少數組織能負擔得起反覆迭代、實驗和改進其定理證明流程。而當成本降至 111 美元時，這一計算完全逆轉。
2025 年至 2026 年間 PutnamBench 結果的快速進步，早已由結合大型語言模型與 Lean 證明檢查引擎的代理工作流程推動。NEAR AI 的方法延續了這一模式，但新增了基準社群此前未曾見過的效率層次。
NEAR AI 將此成就置於更廣泛的基礎設施願景中，該願景以他們所稱的 IronClaw 為核心，這是一個專注於保密且可驗證的人工智慧框架。形式化驗證功能直接契合此框架：若你能在機器層級證明數學論證的正確性，你就為人工智慧系統建立了基礎，使其輸出結果可獨立審計，而非僅憑信任。
NEAR Protocol 決定將 Lean agent 開源，進一步提升了其重要性。通常能帶來 250 倍成本優勢的專有工具都會保持專有性。將 agent 開源意味著此方法論可供任何人檢視、擴展和使用。