erdos-navigator

A toolkit for AI agents working on Paul Erdős's problems. It holds 1,217 problems
with full LaTeX statements — and, uniquely, the record of what AI systems have
already attempted on each one: 538 documented contributions across 405
problems, with outcomes.

Ships with a SQLite database, a CLI, a REST API, a Python SDK, an MCP server, and
Claude Code skills for problem selection, proof technique and self-verification.

Blog post: Erdős Problems and the Coding Agent as Explorer

Why this exists

Finding an open Erdős problem is easy. Finding one that hasn't already been
chewed over by a dozen AI systems is not — and the record of what's been tried
lived only as markdown tables meant for human reading.

That record is now queryable:

./erdos ai 42          # what tried this problem, when, and how it went
./erdos frontier       # open problems nobody's AI has touched — 472 of them
./erdos ai-failed      # open problems where an AI claim turned out wrong

Of 609 open problems, 472 have no recorded AI attempt — 46 of those carry a
prize, and 236 already have a Lean formalization. That's the frontier.

Quick Start

git clone https://github.com/0bserver07/erdos-navigator.git
cd erdos-navigator
pip install -r requirements.txt

The database is included. No scraping, no API keys, no build step.

With Claude Code

cd erdos-navigator
claude

Skills and database are picked up automatically:

> Find an open problem with a Lean formalization that no AI has attempted
> What did GPT-5.5 Pro get wrong on problem #233?
> Use the erdos-solver skill on Problem #137

With any other agent

AGENTS.md covers Codex, Cursor, Copilot, Zed, Windsurf, Aider and friends. Or
register the MCP server for direct tool access:

claude mcp add erdos-navigator -- python $(pwd)/mcp_server/server.py

See mcp_server/README.md for Cursor, Codex and Claude
Desktop config.

Data freshness

Sources differ in age. ./erdos provenance reports the exact state.

erdosproblems.com moved behind Cloudflare bot protection, so statements can't be
refreshed and the old HTML scrapers no longer run (they're kept in
scrapers/legacy/ for reference). Problems #1180–#1217 have complete metadata
but no statement text; the CLI says so rather than showing a blank field.

Refresh the live sources any time:

./erdos sync

CLI

# Problems
./erdos get 42                   # one problem, with its AI attempt history
./erdos find "Sidon set"         # full-text search
./erdos open primes              # open problems by tag
./erdos prizes                   # open problems with prizes
./erdos tags                     # all tags

# AI attempt history
./erdos ai 42                    # every recorded AI attempt on #42
./erdos frontier                 # open, no recorded AI attempt (472)
./erdos frontier --formalized    # ...and already stated in Lean (236)
./erdos frontier --prize         # ...and carrying a prize (46)
./erdos ai-failed                # open problems where an AI claim was wrong (8)
./erdos ai-solved                # problems with a recorded full AI resolution
./erdos ai-stats                 # counts by system and vendor

# Database
./erdos stats                    # overview
./erdos provenance               # per-source freshness
./erdos corpora                  # registered problem corpora
./erdos sync                     # refresh from upstream git

--json works on every read command.

What ./erdos ai looks like

$ ./erdos ai 42
Problem #42 (solved (Lean)) - 3 recorded AI contribution(s)

  🟡 [1(a)] AI standalone
      systems: Codex, GPT-5.2, GPT-5.2 Pro
      date:    19 Jan, 2026
      outcome: 🟡 Partial result (Lean)

  🟢 [1(d)] AI collaborating with humans
      systems: GPT-5.5 Pro
      date:    27 Apr, 2026
      outcome: 🟢 Full solution
      humans:  Harjas Sandhu

  🟢 [2(b)] Formalization
      systems: Codex, GPT-5.5 Pro
      date:    10 May, 2026

Python SDK

from tools.query_db import ErdosDB

with ErdosDB() as db:
    p = db.get_problem("42")
    print(p.statement, p.status, p.tags, p.prize, p.lean_url)
    print(p.ai_attempts, p.ai_best_outcome)   # prior AI work at a glance

    # The frontier: open, untouched by AI, already formalized
    for p in db.get_frontier(formalized=True, limit=10):
        print(p.number, p.statement[:60])

    # What was tried, and what broke
    history = db.get_ai_contributions("42")
    broken = db.get_ai_failures()
    leaderboard = db.get_ai_system_stats()

    # Search
    results = db.full_text_search("Sidon set")
    untouched_primes = db.search(tag="primes", status="open", ai_attempted=False)

    # Know what you're trusting
    for s in db.get_provenance():
        print(s.source, s.as_of, s.status)

REST API

python api/main.py     # http://localhost:8000, interactive docs at /docs

Plus /curated/open-with-prizes, /curated/tractable, /curated/being-worked-on,
/curated/popular, /curated/formalized-open, /tags, /users, /corpora,
/statistics.

MCP Server

Nine tools over the Model Context Protocol — get_problem, search_problems,
get_frontier, get_ai_contributions, find_ai_failures, ai_statistics,
database_statistics, data_provenance, list_corpora.

python mcp_server/server.py

Registration for Claude Code, Claude Desktop, Cursor and Codex is in
mcp_server/README.md.

Architecture

data/erdos_problems.db      SQLite: problems, tags, references, reactions,
                            comments, ai_contributions, ai_systems, corpora,
                            source_provenance
corpus/                     Pluggable corpus framework, git-based sync
  base.py                     Corpus / Source / SyncReport abstractions
  registry.py                 Where corpora are registered
  erdos/                      The Erdős corpus and its four sources
tools/query_db.py           Python SDK — the single query layer
erdos                       CLI
api/main.py                 FastAPI REST service
mcp_server/server.py        MCP server
lean/                       Lean 4 + mathlib project for proofs
.claude/skills/             erdos-solver, math-techniques, lean-formalization
scrapers/legacy/            Retired HTML scrapers

Everything reads through tools/query_db.py. The database is the navigator: the
agent queries it to choose a problem, check what's been tried, pick a technique,
and verify novelty before touching the web.

Other problem corpora

The schema, SDK, CLI, API and MCP server make no assumptions about Erdős
problems. To add another problem set:

1. Implement a Corpus with a CorpusMeta and a list of Sources — copy
   corpus/erdos/ as a template.
2. Register it in corpus/registry.py.
3. python -m corpus.sync --corpus <slug>

Nothing downstream changes. Erdős problems are the only corpus that ships today.

Skills

VERIFICATION.md grades each proof component A–F and carries the community's
red-flag list: a proof that's suspiciously short, proves more than asked, or
doesn't use all the hypotheses is usually solving a misstated problem. It also
notes that models are sycophantic during self-review — ask for refutation, not
assessment.

Worked examples in .claude/examples/:

• #137 (powerful products) — complete proof via case analysis, Pell equations, periodicity mod 45. Rated A/B throughout.
• #108 (chromatic number and girth) — four approaches, all hitting the same barrier at r=5, with the failure points documented.

Statistics

Credits & Attribution

• Paul Erdős (1913–1996) — the problems
• Thomas Bloom — creator of erdosproblems.com
• Terence Tao — maintainer of teorth/erdosproblems and the AI wiki

The AI contribution wiki was built by community contributors who catalogued
hundreds of attempts by hand. This project restructures their work; it doesn't
replace it.

Contributors to erdosproblems.com: Sarosh Adenwalla, Boris Alexeev, Stijn Cambie,
Zachary Chase, Dogmachine, Zach Hunter, Vjekoslav Kovač, Mehtaab Sawhney, Mark
Sellke, Stefan Steinerberger, Wouter van Doorn, Desmond Weisenberg, and many
others. See ATTRIBUTION.md.

How to Cite

@software{erdos-navigator,
  author = {Konrad, Yad},
  title  = {Erd\H{o}s Navigator: API and Toolkit for Erd\H{o}s Mathematical Problems},
  year   = {2026},
  url    = {https://github.com/0bserver07/erdos-navigator},
  note   = {Data from erdosproblems.com (Thomas Bloom) and teorth/erdosproblems (Terence Tao et al.)}
}

When referencing a specific problem, cite the original Erdős paper (listed in
the problem's references) and:

T. F. Bloom, Erdős Problems, https://www.erdosproblems.com

If you use the AI contribution data, also cite the wiki:

Notable cases of AI contributions to Erdős problems,
https://github.com/teorth/erdosproblems/wiki (snapshot of 2026-06-30)

License

• Code: MIT
• Data: from erdosproblems.com and teorth/erdosproblems (Apache 2.0)

Contributing

Fork, branch, open a pull request. For data corrections, contribute to the
upstream repository — this database
syncs from it.