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:

1. The original Erdős paper (listed in each problem's references)
2. 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

1. Fork the repository
2. Create a feature branch
3. Submit a pull request

For data corrections, please contribute to the upstream repository.