Erdős Navigator
activeAgent navigator that turns Claude Code into a theorem proving assistant for 1,179 of Erdős's math problems.
Erdős Navigator
A toolkit that makes all 1,179 of Paul Erdős’s math problems programmatically accessible to coding agents. REST API, CLI, Python SDK, and a set of Claude Code skills sitting on top of a SQLite database.
Why
Most people give their coding agent a blank environment and expect it to figure everything out from training data. That’s like dropping an RL agent into a maze with no map. The navigator gives the agent a structured environment to explore: problems it can query, difficulty signals from the community, Lean formalizations it can verify against, and a workflow that knows when to stop.
What’s in it
- 1,179 problems with full LaTeX statements (651 still open)
- 104 problems with monetary prizes ($37,420 in unsolved bounties)
- Community reactions from erdosproblems.com
- Lean 4 formalization links via Google DeepMind’s formal-conjectures repo
- Full-text search across all problem statements
- Agent-optimized
/agent/suggestendpoint with difficulty scoring
The skills
Claude Code skills define a six-phase workflow: select, understand, pick a technique, attempt, verify, document. The verification skill grades each proof component A-to-F and asks “Would a hostile referee accept this?” The math-techniques library maps problem patterns to known approaches by domain.
I wrote about the thinking behind this in building-erdos-navigator.