Regenerated from the community database (Apache-2.0), dated, and linked back to it
from every problem. erdosproblems.com no longer shows statuses (Bloom's reasons); this is the database's record, not our verdict.
963 of 1221 statements are formalized in Lean (Formal Conjectures) · 107 carry an Erdős prize · 3 are independent of ZFC and 9 more can't be proved, or can't be disproved, from ZFC alone · “open” counts the computable and Lean-checked ones too.
Let \(G\) be a graph given by \(n\) points in \(\mathbb{R}^2\), where any two distinct points are at least distance \(1\) apart, and we draw an edge between two points if they are distance \(1\) apart. Let \(g(n)\) be maximal such that any…
Source: teorth/erdosproblems (its own interactive table), Apache-2.0, pulled 2026-10-24. A status here is what that database records, not an independent verification by us, except where a problem page says so.