+224 since the first snapshot
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.
177 distinct problems since start
Up from 0.9% of resolved problems
86 fewer than in the first snapshot
The resolved share rose from 35.5% to 47.2%. The database grew by 229 problems; unresolved problems went from 640 to 645.
“Resolved” includes proved, disproved, and otherwise solved
Loading chart controls…
How often problems are marked resolved
Each point is a daily average over the previous 30 days
How to read the daily average
Example: 6 status changes over 30 days = 0.2 per day (one every 5 days on average)
Oct 17, 2026 · 1 change to resolved status in the previous 38 days · 0.03 per day on average
Counts changes to existing problems, including repeats. Grey bands mark snapshots more than a week apart; windows may be longer.
Choose a point, or use arrow keys then Enter, to see its changes. Lines mark model releases; select one to compare before and after.
Monthly changes
Download data ↗Resolved status changes and database additions, shown separately. Select a bar to see the problems.
Marked resolvedAdded as resolvedNo longer resolvedRemoved from databaseUnmatched changesNet change
October 2026 (partial month) · 0 net change
View monthly totals
| Month | Marked resolved | Added as resolved | No longer resolved | Removed | Unmatched | Net change |
|---|---|---|---|---|---|---|
| 2025-09 (partial) | 6 | 17 | 0 | 0 | 0 | +23 |
| 2025-10 | 28 | 7 | -3 | 0 | 0 | +32 |
| 2025-11 | 3 | 0 | 0 | 0 | 0 | +3 |
| 2025-12 | 21 | 9 | -3 | 0 | 0 | +27 |
| 2026-01 | 28 | 8 | 0 | -1 | 0 | +35 |
| 2026-02 | 8 | 0 | 0 | 0 | 0 | +8 |
| 2026-03 | 8 | 1 | 0 | 0 | 0 | +9 |
| 2026-04 | 22 | 11 | 0 | 0 | 0 | +33 |
| 2026-05 | 19 | 0 | 0 | 0 | 0 | +19 |
| 2026-06 | 3 | 0 | 0 | 0 | 0 | +3 |
| 2026-07 | 12 | 0 | 0 | 0 | 0 | +12 |
| 2026-08 | 5 | 0 | 0 | 0 | 0 | +5 |
| 2026-09 | 14 | 1 | 0 | 0 | 0 | +15 |
| 2026-10 (partial) | 0 | 0 | 0 | 0 | 0 | +0 |
Resolved problems in Lean
The shaded gap shows resolved problems with no Lean solution recorded
ResolvedOf those, in Lean
Oct 17, 2026 · 576 resolved · 313 of those in Lean (54.3%) · 263 without Lean formalization
Excludes problems still listed as unresolved
Before and after a model release
Compare observed changes to resolved across two 30-day windows around the release date. The data does not tell us whether the model helped.
Choose a release to compare
Choose a release to compare
Why timing is uncertain
The lower count includes changes whose whole snapshot interval is inside the window. The upper count also includes changes that could fall on either side of a boundary. The same uncertain changes may appear in both ranges; do not add the upper counts.
Windows use UTC dates, not launch times. Ranges cover only changes captured between saved snapshots; missed changes are not estimated. Nearby release windows can overlap.
What changed
1 changes across 1 distinct problems
Changes to resolved between the snapshots on Sep 9, 2026 and Oct 17, 2026 (38 days)
| Problem | Recorded on | Change | Between snapshots | Source |
|---|---|---|---|---|
| #547 | 2026-09-18 | Marked resolved | 2026-09-09 → 2026-09-18 | View revisions ↗ |
Problem links show today’s page. “View revisions” shows the historical changes. Repeated changes count separately.