Erdős Problems

1,217 source-owned questions · 604 with a formal statement · searchable by statement, number, topic and source status.

Add a contribution Collection details

Collection coverage

Source status, exact formal material, and reviewed Results are separate signals.

Open per source608
Resolved per source556
Other source status53

Exact formal statement available604 / 1,217

With Repository-reviewed evidence2 / 1,217

61 Problems

2/2

Number	Question	Source says	Formal	Result here
#921	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#922	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#923	Is it true that, for every $k$ , there is some $f(k)$ such that if $G$ has chromatic number $\geq f(k)$ then $G$ contains a triangle-free subgraph with chromatic number $\geq k$ ?proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#944	Let $k \ge 4$ and $r\ge 1$ . Must there exist a graph $G$ with chromatic number $k$ such that every vertex is critical, yet every critical set of edges has size $>r$ ?openFormalized	open	In Lean	No Result decision
#1032	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1068	Does every graph with chromatic number $\aleph_1$ contain a countable subgraph which is infinitely connected?openFormalized	open	In Lean	No Result decision
#1091	No statement retained — open to read what the source holdssolvedNo formal declaration	solved	No formal statement	No Result decision
#1092	Is it true that $f_2(n) \gg n$ ? Disproved by Rödl, who showed $f_r(n) = o(n)$ for all fixed $r \geq 2$ . A conjecture of Erdős, Hajnal, and Szemerédi.disprovedFormalized	disproved	In Lean	No Result decision
#1104	Lower bound (Hefty–Horn–King–Pfender 2025). There exists a constant $c_1 \in (0,1]$ such that, for sufficiently large $n$ , $c_1 \sqrt{\frac{n}{\log n}} \le f(n),$ where $f(n)$ denotes the maximum chromatic number of a triangle-free graph on $n$ vertices, formalized as `triangleFreeMaxChromatic n`.openFormalized	open	In Lean	No Result decision
#1156	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1175	Let $\kappa$ be an uncountable cardinal. Must there exist a cardinal $\lambda$ such that every graph with chromatic number $\lambda$ contains a triangle-free subgraph with chromatic number $\kappa$ ?openFormalized	open	In Lean	No Result decision
#1176	Let $G$ be a graph with chromatic number $\aleph_1$ . Is it true that there is a colouring of the edges with $\aleph_1$ many colours such that, in any countable colouring of the vertices, there exists a vertex colour containing all edge colours?not disprovableFormalized	not disprovable	In Lean	No Result decision
#1177	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision

Problems

Search problems.science