Erdős problems in the AI era

See which Erdős problems have been resolved and which solutions have been checked in Lean.

Dates track database updates. AI release dates do not tell us which model, if any, helped solve a problem.

What do “resolved” and “Lean” mean?

Resolved includes problems that have been proved, disproved, or otherwise solved. The remaining statuses are grouped as open or unresolved.

Lean is software for checking mathematical proofs. Writing a problem’s statement in Lean is different from checking a solution. A Lean solution may be listed before the database’s resolved status is updated.

Source data on GitHub

Snapshot:

Source revision
See recent changes Download SVG
Total problems1,221

Recorded at this date.

Resolved576

Proved, disproved, or otherwise solved.

Solutions in Lean318

Across all problem statuses.

Explore earlier snapshots

Choose a date or press Play to see how the database changed. Dots mark AI model releases.

EarlierLatest

Loading historical snapshots…

How the problems break down

Read from left to right: all problems, their status, then whether a solution is recorded in Lean.

Share of all problems

Scroll sideways to explore the diagram, or read the data table

Erdős problems: status and Lean formalization 1,221 problems divide into 576 resolved and 645 open or unresolved. Layout by D3 Sankey. Bar heights and ribbon widths are proportional to counts. A text table follows the chart. Data: Erdős problems database contributors, maintained by Thomas Bloom and Terence Tao. Source: https://github.com/teorth/erdosproblems/blob/f4b678341eaf36425d3ab35491a4e5b16bc4a0d9/data/problems.yaml. Snapshot: 2026-10-17. Visualization: Jason Willems. Layout: D3 Sankey. All problems → Resolved: 576 All problems → Open / unresolved: 645 Resolved → Proved: 336 Proved → Lean-formalized proof: 183 Proved → Not Lean-formalized: 153 Resolved → Disproved: 139 Disproved → Lean-formalized disproof: 97 Disproved → Not Lean-formalized: 42 Resolved → Otherwise solved: 101 Otherwise solved → Lean-formalized solution: 33 Otherwise solved → Not Lean-formalized: 68 Open / unresolved → Completely open: 593 Open / unresolved → Decidable: 8 Open / unresolved → Falsifiable: 25 Open / unresolved → Verifiable: 7 Open / unresolved → Not provable in ZFC: 3 Open / unresolved → Not disprovable in ZFC: 6 Open / unresolved → Independent of ZFC: 3 All problems: 1,221 (100.0% of all problems) Resolved: 576 (47.2% of all problems) Open / unresolved: 645 (52.8% of all problems) Proved: 336 (27.5% of all problems) Lean-formalized proof: 183 (15.0% of all problems) Not Lean-formalized: 153 (12.5% of all problems) Disproved: 139 (11.4% of all problems) Lean-formalized disproof: 97 (7.9% of all problems) Not Lean-formalized: 42 (3.4% of all problems) Otherwise solved: 101 (8.3% of all problems) Lean-formalized solution: 33 (2.7% of all problems) Not Lean-formalized: 68 (5.6% of all problems) Completely open: 593 (48.6% of all problems) Decidable: 8 (0.7% of all problems) Falsifiable: 25 (2.0% of all problems) Verifiable: 7 (0.6% of all problems) Not provable in ZFC: 3 (0.2% of all problems) Not disprovable in ZFC: 6 (0.5% of all problems) Independent of ZFC: 3 (0.2% of all problems) Resolved 576 47.2% Open / unresolved 645 52.8% Not Lean-formalized 153 12.5% Not Lean-formalized 42 3.4% Not Lean-formalized 68 5.6%
Wider bands mean more problems. The open and unresolved categories are separate statuses, not steps toward a proof.

Problem status

Snapshot: October 17, 2026“Problems”: % of all problems. Lean columns: % within each status. A dash means no data or an empty status.

StatusProblemsLean-formalizedNot Lean-formalized
Proved336 (27.5%)183 (54.5%)153 (45.5%)
Disproved139 (11.4%)97 (69.8%)42 (30.2%)
Otherwise solved101 (8.3%)33 (32.7%)68 (67.3%)
Completely open593 (48.6%)——
Decidable8 (0.7%)——
Falsifiable25 (2.0%)——
Verifiable7 (0.6%)——
Not provable in ZFC3 (0.2%)——
Not disprovable in ZFC6 (0.5%)——
Independent of ZFC3 (0.2%)——
All problems1,221 (100.0%)——
More about these problems: prizes, Lean statements, and integer sequences

These groups overlap. OEIS is the Online Encyclopedia of Integer Sequences.

Solutions formalized in Lean

318
313 resolved; 5 still unresolved

A Lean solution may be recorded before a human reviews it and updates the status

Linked to OEIS

358
problems linked to 474 integer sequences in OEIS, through 558 links

107 sequences added since this database began (A387000 onwards)

Possible OEIS links

310
problems with potential OEIS links not yet listed here

235 currently have no OEIS links

Related sequences being submitted to OEIS

0

Literature reviews requested

0

Ambiguous statements

11
problems have ambiguous statements