数学で最も厳しいベンチマークのすべての問題を解決するには通常数万ドルかかるところ、NEAR AIはたった111ドルでそれを実現しました。
2026年9月6日、NEAR Protocolの共同創設者であるアレックス・スキダノフは、プロジェクトのオープンソースのLeanエージェントが、ウィリアム・ローウェル・プタナム数学コンペティションから抽出されたベンチマークであるPutnamBenchの全672問を解決したと発表しました。総費用は111ドルでした。次に安かった既知の提出物は、この金額の250倍かかりました。
PutnamBenchとは何か、そしてそれがなぜ重要なのか
プタムコンペティションは北米で最も権威のある大学院生向け数学コンテストです。優れた学生であっても、得点がゼロになることは珍しくありません。この試験は、あなたを打ちのめすように設計されています。
2024年に導入されたPutnamBenchは、その難易度の伝統をAI定理証明器のための正式な評価スイートに変換したものです。このベンチマークには、数学的議論を機械検証可能な精度で記述する必要がある証明支援言語Lean 4でエンコードされた672の問題が含まれています。論理的に不正確な証明は、部分点なしで即座に却下されます。
NEAR AIの結果が出る前は、PutnamBenchを試行するエージェントが問題1つあたりしばしば数千回の推論呼び出しを必要としていました。計算コストは急速に積み上がり、主要なシステムでの完全なベンチマーク実行の総費用は1万ドルから2万5千ドルの範囲になりました。
NEAR AIのLeanエージェントが、672問の問題セットを111ドルで完了しました。
なぜコスト差が本当の話題なのか
1回のフルランに1万ドルから2万5千ドルかかるため、理論証明パイプラインを繰り返し改善・実験できる組織は限られていました。しかし、111ドルになると、この状況は完全に逆転します。
2025年から2026年にかけてのPutnamBench結果の急速な進歩は、大規模言語モデルとLeanの証明検証エンジンを組み合わせたエージェントワークフローによってすでに推進されていました。NEAR AIのアプローチはこのパターンを拡張し、ベンチマークコミュニティがこれまで見たことのない効率性の層を追加しています。
NEAR AIは、この成果を「IronClaw」と呼ぶフレームワークを中心に据えた広範なインフラ構想の一部として位置づけている。IronClawは、機密性と検証可能なAIを軸としている。形式的検証機能はこの枠組みに直接適合する：機械レベルで数学的論証が正しいことを証明できれば、信仰に基づくのではなく、出力結果を独立して監査可能なAIシステムの基盤が得られる。
NEAR ProtocolがLeanエージェントをオープンソース化することにより、その重要性がさらに高まっている。250倍のコスト優位性をもたらす独自ツールは通常、独自のまま保持される。エージェントをオープンソース化することで、その方法論が誰でも確認、拡張、利用できるようになる。