NEAR AI solves all 672 PutnamBench problems for $111

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 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 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.