# NEAR AI solves all 672 PutnamBench problems for $111 > NEAR Protocol said the open-source theorem-proving agent completed the Lean 4 benchmark at 1/250 the cost of the next-cheapest complete submission. The official leaderboard gives NEAR AI the lowest mean cost among three 672-problem runs. - Publication: Go Big News - By Go Big News Staff (Staff News) - Category: AI - Published: 2026-09-07T04:14:55.796+00:00 - Canonical: https://www.gobignews.com/ai/near-ai-solves-all-672-putnambench-problems-for-111 --- [NEAR AI](https://near.ai) solved all 672 Lean 4 problems in PutnamBench for $111, NEAR Protocol said in a post on X on Sept. 6, 2026. The account said the open-source agent cost 250 times less than the next-cheapest complete submission. NEAR Protocol said the lower cost makes formal verification cheap enough to run on every software commit. It also said anyone can inspect the verifier used to check the agent’s work. [PutnamBench](https://github.com/trishullab/PutnamBench) evaluates theorem-proving algorithms using problems from the William Lowell Putnam Mathematical Competition between 1962 and 2025. It records 672 formalizations in Lean 4, 640 in Isabelle and 412 in Coq. A paper accepted at NeurIPS 2024 describes the Putnam as North America’s premier undergraduate mathematics competition. The official leaderboard added “NEAR AI (w/ DeepSeek V4)” on Sept. 4 with 672 of 672 Lean problems solved. It reports a mean cost of $0.17 per problem, a median of $0.04 and a maximum of $11.18. Humanfia averaged $44.50 per problem, while Logical Intelligence’s Aleph Prover averaged $74. Both also reported 672 solves. The [public agent repository](https://github.com/SkidanovAlex/putnambench-deepseek) reports a billed total of $111.85 across 724 attempts. DeepSeek V4 Flash produced 653 successful proofs and V4 Pro produced 19. Two problems used corrected upstream formalizations. The harness gives the agent a Lean file containing a `sorry` placeholder and access to bash. It continues until a verifier confirms that the proof contains no `sorry` or extra axioms and that its theorem statement matches the frozen original. The leaderboard says the solution bundle was shared privately for independent verification, while a green heart identifies the method as fully open-sourced. The announcement quoted Alex Skidanov, a NEAR Protocol co-founder working on formal verification of code. NEAR’s official history says Skidanov and Illia Polosukhin started the original NEAR AI in 2017 to develop models that could write code from natural-language descriptions. NEAR Protocol announced NEAR AI as a decentralized-AI research and development lab led by the two founders in May 2024. --- ## Companies in this story - Near: https://www.gobignews.com/company/nearai --- ## X profiles in this story - @nearprotocol: https://www.gobignews.com/profile/nearprotocol