Erdos Navigator — plugin by 0bserver07

Explore and tackle 1,179 open mathematical problems posed by Paul Erdős using AI agents.

A toolkit for AI agents to explore and attempt Paul Erdős's 1,179 open mathematical problems. Includes a SQLite database, REST API, CLI, Python SDK, and Claude Code skills for problem selection, proof techniques, solution attempts, and self-verification.

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

Features

1,179 problems with full LaTeX statements, community reactions, and discussion threads
Full-text search, tag filtering, and curated query endpoints
REST API (FastAPI) and Python SDK for direct database access
Lean 4 project (lean/) with mathlib for formalizing proofs
Lean formalization links for 354 problems (via DeepMind's formal-conjectures)
Claude Code skills for problem-solving workflows and proof verification

Quick Start

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

That's it. The database is included - no scraping needed.

Use with Claude Code

cd erdos-navigator
claude

The skills and database are picked up automatically. Try:

> Use the erdos-solver skill to find a tractable open problem
> What open problems involve Sidon sets?
> Attempt Problem #137

Start the API

python api/main.py
# or
uvicorn api.main:app --reload

API available at http://localhost:8000

API Endpoints

Core Endpoints

Endpoint	Description
`GET /problems`	List problems with filters
`GET /problems/{number}`	Full problem details
`GET /problems/{number}/comments`	Problem discussion
`GET /search?q={query}`	Full-text search
`GET /tags`	All tags with counts
`GET /statistics`	Database statistics

Filter Parameters

GET /problems?status=open&tag=primes&has_prize=true&limit=20

status: open, proved, disproved, solved, etc.
tag: number theory, graph theory, primes, etc.
has_prize: true/false
formalized: true/false
has_reactions: true/false
reaction_type: like, working_on, hard, easy, collab

Curated Endpoints

Endpoint	Description
`GET /curated/open-with-prizes`	Open problems with monetary prizes
`GET /curated/tractable`	Problems marked "tractable" by community
`GET /curated/being-worked-on`	Problems users are actively working on
`GET /curated/popular`	Most engaged problems
`GET /curated/formalized-open`	Open problems with Lean formalizations

For AI Agents

GET /agent/suggest?difficulty=medium&tag=primes&formalized=true

Returns a suggested problem with context for AI agents to work on.

CLI Tool

./erdos stats                    # Database statistics
./erdos get 42                   # Get problem #42
./erdos get 42 --json            # JSON output
./erdos open primes              # Open problems about primes
./erdos prizes                   # Problems with prizes
./erdos find "arithmetic"        # Full-text search
./erdos tags                     # All tags

Python SDK

from tools.query_db import ErdosDB

with ErdosDB() as db:
    # Get a specific problem
    p = db.get_problem("42")
    print(p.statement)
    print(p.reactions)  # {'like': ['user1'], 'working_on': ['user2']}

    # Search
    results = db.full_text_search("Sidon set")

    # Curated queries
    tractable = db.get_tractable_problems()
    popular = db.get_popular_problems(10)
    working = db.get_problems_being_worked_on()

Architecture

SQLite DB (1,179 problems)
    ├── CLI (./erdos)
    ├── REST API (FastAPI)
    ├── Python SDK (tools/query_db.py)
    ├── Lean 4 Project (lean/)
    │       └── ErdosProofs/     → mathlib-based proof files
    └── Claude Code Skills (.claude/skills/)
            ├── erdos-solver          → 6-phase problem-solving workflow
            ├── math-techniques       → proof technique library by domain
            ├── lean-formalization    → Lean 4 formalization workflow
            └── verification          → proof audit + novelty checking

The database is the navigator. The agent queries it to find problems, select techniques, and verify novelty before searching the web. See the blog post for the motivation behind this design.

Skills & Workflow

The .claude/skills/ directory provides structured workflows for AI agents working on Erdős problems.

erdos-solver

Six phases: select a problem, understand it, pick a technique, attempt a solution, run the post-solution pipeline, document results.

The post-solution pipeline grades every proof component A through F, checks novelty against local data before hitting the web, and only claims a result after it survives a hostile-referee test.

math-techniques

Proof technique library organized by domain:

Domain	Techniques
Number theory	Pell equations, modular arithmetic, p-adic analysis, density arguments
Combinatorics	Probabilistic method, Ramsey theory, extremal arguments, double counting
Graph theory	Chromatic numbers, spectral methods, Turán-type arguments
Geometry	Incidence geometry, lattice constructions, polynomial methods

lean-formalization

Workflow for formalizing proofs in Lean 4. Checks whether a problem has an existing formal statement, walks through translating to mathlib types, and handles the lake build iteration loop. LEAN_PATTERNS.md has type mappings and a tactic cheat sheet.

verification

Grading framework that rates each proof component A (formal-ready) through F (unverified claim). Tracks AI-solved problems in LITERATURE.md to prevent rediscovery claims.

Example attempts

Documented solution attempts live in .claude/examples/:

Problem #137 (powerful products) — complete proof using case analysis, Pell equations, and periodicity mod 45. Rated A/B across all components. Likely novel, pending peer review.
Problem #108 (chromatic number and girth) — four approaches attempted, all hitting the same barrier at r=5. Documented exactly where and why each approach fails.

Database Schema

Main Tables

problems - Problem statements and metadata
tags / problem_tags - Classification
problem_references - Bibliography links
problem_reactions - User engagement (like, working_on, hard, easy, etc.)
contributors - Problem contributors
comments - Discussion threads

Key Fields

Field	Description
`statement`	LaTeX problem text
`status`	open, proved, disproved, solved, etc.
`prize`	Prize amount or "no"
`lean_url`	Link to Lean formalization
`oeis`	Related OEIS sequences
`reactions`	Community engagement by type

Updating Data

# Full update
python scrapers/update_all.py

# Quick update (skip comments)
python scrapers/update_all.py --quick

# Comments only
python scrapers/update_all.py --comments

# Pull latest YAML first
python scrapers/update_all.py --pull

Data Sources

Primary: erdosproblems.com - Problem statements, reactions, comments
YAML data: github.com/teorth/erdosproblems - Structured metadata (maintained by Terence Tao)
Formalizations: Google DeepMind formal-conjectures

Data Updates

The database (data/erdos_problems.db) is included in this repo - no scraping needed.

To refresh with latest data:

./setup.sh

The source YAML repo (teorth/erdosproblems) is maintained by Terence Tao and cloned fresh during updates.

Statistics

Metric	Count
Total problems	1,179
Open problems	651
With prizes	104
Formalized (Lean)	354
Total reactions	526
Unique users	81
Total contributors	582

Credits & Attribution

Data Sources

Source	Description	License
erdosproblems.com	Problem statements, reactions, comments	-
teorth/erdosproblems	Structured YAML metadata	Apache 2.0
Google DeepMind formal-conjectures	Lean formalizations	-

People

Paul Erdős (1913-1996) - Original problems
Thomas Bloom - Creator of erdosproblems.com
Terence Tao - Maintainer of teorth/erdosproblems

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 for full details.

How to Cite

If you use this database in research, publications, or if an AI agent solves a problem using this data:

Cite This Repository

BibTeX:

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

Plain text:

Yad Konrad. Erdős Navigator (2026). https://github.com/0bserver07/erdos-navigator
Data sourced from erdosproblems.com (Thomas Bloom) and teorth/erdosproblems (Terence Tao et al.)

Cite the Original Problem

When referencing a specific Erdős problem, also cite:

The original Erdős paper (listed in each problem's references)

erdosproblems.com:

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

Example Citation (AI Agent Solving a Problem)

If an AI agent finds a solution to Problem #42:

We used the Erdős Navigator [1] to identify and retrieve Problem #42,
originally posed by Erdős in [Er95]. The problem data was sourced from
erdosproblems.com [2] and the teorth/erdosproblems repository [3].

[1] Erdős Navigator, https://github.com/0bserver07/erdos-navigator
[2] T. F. Bloom, Erdős Problems, https://www.erdosproblems.com/42
[3] T. Tao et al., teorth/erdosproblems, https://github.com/teorth/erdosproblems

License

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

Contributing

Fork the repository
Create a feature branch
Submit a pull request

For data corrections, please contribute to the upstream repository.