nearai

Putnambench Deepseek — Development skill for Claude Code

Development community

An agent that solved all 672 putnambench problems.

How to install Putnambench Deepseek

This entry records only its repository, not the path inside it, so there is no exact command to give. Open nearai/putnambench-deepseek and copy the folder into ~/.claude/skills/, or the file into ~/.claude/agents/.

What Putnambench Deepseek does

An agent that solved all 672 putnambench problems.

Alternatives in Development

IPolloWork — Enterprise-grade, local-first Agent Workbench for people and agent teams 4.9k ★
Petdex — A public gallery of animated pets for Codex, Claude Code, DeepSeek Harness, Hermes, OpenCode, Gemini CLI, and 4k ★
Dao Code — Open-source TypeScript terminal coding agent for DeepSeek-V4 — builds on DeepSeek's strong price-performance a 1.3k ★

README

putnambench-deepseek

An autonomous DeepSeek-driven agent that solved PutnamBench in Lean 4: **672 problems solved and machine-validated** — all 670 solvable upstream problems it attempted, plus corrected variants of the two problems whose upstream formalizations turned out to be defective (below).

The agent harness provides the agent with the given Lean file with a `sorry`, and access to a single tool: bash (plus tools to report that the work is done). All other operations, such as reading and writing files or invoking Lean, must be done via the bash tool. Claude Code-generated instructions on how to approach the task are given in the system prompt (see section "Strategy" in `run_putnam_solver.py`), but no orchestration is done by the harness other than that: all that the harness does is the classic agent loop of "call LLM, execute tools, repeat".

The `completed` tool verifies that the problem is solved, and if so, reports to the outer system, which then re-verifies the solution and records it.

In the first pass we ran each problem using DeepSeek V4 Flash 0731, with no time or turn limit. The agent ran until it either successfully solved the problem, or emitted a turn with no tool calls. This resulted in proving 639 problems. We then reran exactly the same model and the same harness on the remaining problems, which resulted in a further 22 solved problems.

For the third run, only 11 problems remained, and manual inspection of trajectories was possible. We identified that two problems had issues with formalization (one had a bogus statement, and one had a correct statement, but an incorrect answer), and that the remaining 9 agents ended their trajectories giving up. For the former, we used Claude Code to fix the problems (see below), and for the latter, we removed the ability for the agent to stop without completing the proof. If on a particular turn the agent doesn't emit any tool calls, the harness emits a user message with a nudge, and continues querying th