Erdős Problems Database

Track problem statuses and Lean formalizations over time.

Source data on GitHub

1,217 problems

Source revision
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,217 problems divide into 574 resolved and 643 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/5ca6b58dccc3e7a41d7db5f2cafdb944599edc4c/data/problems.yaml. Snapshot: 2026-09-09. Visualization: Jason Willems. Layout: D3 Sankey. All problems → Resolved: 574 All problems → Open / unresolved: 643 Resolved → Proved: 334 Proved → Lean-formalized proof: 176 Proved → Not Lean-formalized: 158 Resolved → Disproved: 139 Disproved → Lean-formalized disproof: 91 Disproved → Not Lean-formalized: 48 Resolved → Otherwise solved: 101 Otherwise solved → Lean-formalized solution: 29 Otherwise solved → Not Lean-formalized: 72 Open / unresolved → Completely open: 591 Open / unresolved → Decidable: 9 Open / unresolved → Falsifiable: 25 Open / unresolved → Verifiable: 7 Open / unresolved → Not provable in ZFC: 3 Open / unresolved → Not disprovable in ZFC: 4 Open / unresolved → Independent of ZFC: 4 All problems: 1,217 (100.0% of all problems) Resolved: 574 (47.2% of all problems) Open / unresolved: 643 (52.8% of all problems) Proved: 334 (27.4% of all problems) Lean-formalized proof: 176 (14.5% of all problems) Not Lean-formalized: 158 (13.0% of all problems) Disproved: 139 (11.4% of all problems) Lean-formalized disproof: 91 (7.5% of all problems) Not Lean-formalized: 48 (3.9% of all problems) Otherwise solved: 101 (8.3% of all problems) Lean-formalized solution: 29 (2.4% of all problems) Not Lean-formalized: 72 (5.9% of all problems) Completely open: 591 (48.6% of all problems) Decidable: 9 (0.7% of all problems) Falsifiable: 25 (2.1% of all problems) Verifiable: 7 (0.6% of all problems) Not provable in ZFC: 3 (0.2% of all problems) Not disprovable in ZFC: 4 (0.3% of all problems) Independent of ZFC: 4 (0.3% of all problems) Resolved 574 Open / unresolved 643 Not Lean-formalized 158 Not Lean-formalized 48 Not Lean-formalized 72
Bar heights and flow widths show problem counts. Attributes overlap and are counted separately. Chart: D3 Sankey.

Problem status

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

StatusProblemsLean-formalizedNot Lean-formalized
Proved334 (27.4%)176 (52.7%)158 (47.3%)
Disproved139 (11.4%)91 (65.5%)48 (34.5%)
Otherwise solved101 (8.3%)29 (28.7%)72 (71.3%)
Completely open591 (48.6%)——
Decidable9 (0.7%)——
Falsifiable25 (2.1%)——
Verifiable7 (0.6%)——
Not provable in ZFC3 (0.2%)——
Not disprovable in ZFC4 (0.3%)——
Independent of ZFC4 (0.3%)——
All problems1,217 (100.0%)——