erdos-solver

name	erdos-solver
description	Workflow for attempting to solve Erdős problems. Use when the user wants to work on a specific Erdős problem, analyze open problems, or find tractable problems to attempt.

Erdős Problem Solver Workflow

A structured approach to working on Erdős problems, informed by AI research efforts (Gemini/Aletheia, GPT-5 series, Aristotle) and by the guidance the Erdős problems community published on its AI wiki.

Before anything else: check what has already been tried

405 of 1,217 problems already have a recorded AI attempt. Skipping this step is the single most common way to waste an afternoon.

./erdos ai {number}          # every recorded AI attempt on this problem
./erdos provenance           # how stale is the local data

Read the outcome column carefully:

Outcome	What it means for you
🟢 full	Likely resolved. Verify at erdosproblems.com before spending effort.
🟡 partial	Progress exists. Read it — the remaining gap is your target.
🔴 incorrect	An attempt broke here. Understand why before repeating the approach.
⚪ unverified	Claimed but unchecked. Verifying it is itself useful work.
(nothing)	Genuinely untouched. 472 open problems are in this state.

Data caveat: statements and comments are a 2026-02-01 snapshot; the AI wiki froze 2026-06-30. Status/prize/tags/formalization are current. Always confirm a problem is still open at https://www.erdosproblems.com/{number} before investing serious effort.

Phase 1: Problem Selection

./erdos frontier                      # open, no recorded AI attempt
./erdos frontier --formalized         # ...and already stated in Lean (236)
./erdos frontier --prize              # ...and carrying a prize (46)
./erdos ai-failed                     # open problems where AI got it wrong (8)

from tools.query_db import ErdosDB

with ErdosDB() as db:
    frontier = db.get_frontier(formalized=True, limit=25)   # untouched + Lean
    tractable = db.get_tractable_problems()                 # community-marked easy
    formalized = db.get_formalized_open()                   # open + Lean statement
    primes = db.search(tag="primes", status="open")         # by tag
    active = db.get_problems_being_worked_on()              # humans already on it
    broken = db.get_ai_failures()                           # AI claimed, was wrong

Selection criteria

Factor	Why it matters
No recorded AI attempt	You are not retreading published work
Has Lean formalization	Statement is unambiguous and machine-checkable
Tagged "formalisable"	Community thinks it is well-defined
Recent comments	Active discussion, partial progress available
Status = "open"	Actually unsolved — but re-verify upstream

Two under-rated starting points: problems where an AI attempt was recorded incorrect (./erdos ai-failed), and problems with a partial result where the remaining gap is explicit.

Phase 2: Deep Understanding

p = db.get_problem(number)
print(p.statement)                       # full LaTeX
print(p.references)                      # original Erdős papers
print(p.lean_url)                        # formal statement, if any
print(p.ai_attempts, p.ai_best_outcome)  # prior AI work at a glance
for c in db.get_comments(number):        # community discussion
    print(c.author, c.content)

Understand the intent

Common failure modes:

• Notational conventions differ (additive vs Dirichlet convolution)
• "Strong" vs "weak" completeness
• Implicit assumptions in Erdős's original formulation
• Transcription errors from the original papers

You can solve the wrong version of a problem without noticing. Read the original source, not only the database statement.

Literature review

~40% of "novel" AI solutions were already in the literature (Gemini study). Forward and backward citation searches from the papers listed on the problem page are the highest-yield move. Google Scholar, MathSciNet, zbMATH, OEIS.

Phase 3: Technique Selection

• NUMBER_THEORY.md
• COMBINATORICS.md
• GRAPH_THEORY.md
• GEOMETRY.md

Problem pattern	Try first
"Are there infinitely many..."	Construction, Pell equations
"Does there exist..."	Probabilistic method
"For all n, is it true..."	Induction, counterexample search
"What is the maximum..."	Extremal arguments
"Can we color..."	Ramsey theory
"How many distinct..."	Incidence geometry

Phase 4: Solution Attempt

1. Check small cases (n = 1, 2, 3, …)
2. Look for counterexamples if the conjecture seems false
3. Try the direct approach before the clever one

Informal sketch → Detailed proof → Formal verification (if Lean available)

Record approaches tried, why they failed, partial progress, and related problems that might transfer. A well-documented failure is a real contribution — see .claude/examples/solution_attempt_108.md.

Phase 5: Post-Solution Pipeline

Follow POST_SOLUTION.md:

SOLUTION → Self-Audit → Novelty Check → Formalize → Peer Review → Submit

5.1 Self-audit

Use the VERIFICATION.md checklist and rate each component A–F. Its red-flag list is drawn from the community's own guidance and is the part most worth internalising.

5.2 Novelty check — local data first

./erdos ai {number}                                     # 1. prior AI attempts
./erdos get {number} --json                             # 2. status, references
grep -i "{number}" .claude/skills/math-techniques/LITERATURE.md   # 3. known AI solutions
ls .claude/examples/solution_attempt_*.md               # 4. our own prior work
# 5. ONLY THEN: web search for recent literature

5.3 Formalization

./erdos get {number} --json | jq -r .lean_url

If a Lean statement exists, use it — but note the community's warning: the statement should be formalized by a human or third party, not by the same AI producing the proof, or you risk formalizing a misstatement into a proof.

See lean-formalization.

Phase 6: Documentation

### Sources
- [Erdős Problem #N](https://www.erdosproblems.com/N)
- Original: [reference from ./erdos output]
- Prior AI work: [from ./erdos ai N]
- **This attempt**: `.claude/examples/solution_attempt_N.md`

Outcome	Action
Solved	Post to erdosproblems.com after due diligence — see POST_SOLUTION.md
Partial	Document progress and the precise remaining gap
Literature	Report the reference so the database can be updated

Pitfalls

1. Not checking prior AI attempts — ./erdos ai N takes one second
2. Assuming "open" means unsolved — local status can lag upstream
3. Misinterpreting the statement — read the original Erdős paper
4. Ignoring definitional conventions — check the site's notation guide
5. Claiming novelty prematurely — AI solutions often rediscover known results
6. Trusting your own review — models are sycophantic; ask for refutation, not approval
7. Rushing to announce — several AI "solutions" were walked back days later