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.
908 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.
PROVED LEANPRIZE $500combinatorics · intersecting family
Let \(f(n)\) be minimal such that there is an intersecting family \(\mathcal{F}\) of sets of size \(n\) (so \(A\cap B\neq\emptyset\) for all \(A,B\in \mathcal{F}\)) with \(\lvert \mathcal{F}\rvert=f(n)\) such that any set \(S\) with…
DISPROVED LEANPRIZE $10number theory · intersecting family
Suppose \(A \subseteq \{1,\dots,N\}\) is such that there are no \(k+1\) elements of \(A\) which are relatively prime. An example is the set of all multiples of the first \(k\) primes. Is this the largest such set? To avoid trivial…
What is the largest possible subset \(A\subseteq\{1,\ldots,N\}\) which contains \(N\) such that \(\mathrm{gcd}(a,b)>1\) for all \(a\neq b\in A\)? Erdős conjectured that if \(N=q_1^{k_1}\cdots q_r^{k_r}\) (where \(q_1<\cdots <q_r\) are…
Let \(\mathcal{F}\) be a family of sets closed under taking subsets (i.e. if \(B\subseteq A\in\mathcal{F}\) then \(B\in \mathcal{F}\)). There exists some element \(x\) such that whenever \(\mathcal{F}'\subseteq \mathcal{F}\) is an…
Let \(A\subseteq \{1,\ldots,N\}\) be such that, for all \(a,b\in A\), the product \(ab\) is not squarefree. Is the maximum size of such an \(A\) achieved by taking \(A\) to be the set of even numbers and odd non-squarefree numbers? A…
Source: teorth/erdosproblems (its own interactive table), Apache-2.0, pulled 2026-10-21. A status here is what that database records, not an independent verification by us, except where a problem page says so.