Erdős problems in the AI era

Explore recorded resolutions and formalized proofs over time, alongside AI model releases

Dates show database updates, not necessarily when the mathematics was done. Release markers provide context, not attribution.

Source data on GitHub

1,221 problems

Source revision
See recent changes Download SVG
EarlierLatest

Loading historical snapshots…

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/6754c649e41328f461412eb1d08ea72f1d4bb5d1/data/problems.yaml. Snapshot: 2026-09-28. 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 Open / unresolved 645 Not Lean-formalized 153 Not Lean-formalized 42 Not Lean-formalized 68
Bar heights and flow widths show problem counts. Attributes overlap and are counted separately. Chart: D3 Sankey.

Problem status

Snapshot: September 28, 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%)——