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

275 Problems

1/6

Number	Question	Source says	Formal	Result here
#19	No statement retained — open to read what the source holdsdecidableNo formal declaration	decidable	No formal statement	No Result decision
#22	Let $\epsilon > 0$ and let $n$ be sufficiently large depending on $\epsilon$ . Is there a graph on $n$ vertices with at least $n^2/8$ many edges which contains no $K_4$ , such that the largest independent set has size at most $\epsilon n$ ?provedFormalized	proved	In Lean	No Result decision
#23	The blow-up of $C_5$ shows that the bound $n^2$ in Erdős Problem 23 is tight: any bipartite subgraph must omit at least $n^2$ edges.falsifiableFormalized	falsifiable	In Lean	No Result decision
#24	Does every triangle-free graph on $5n$ vertices contain at most $n^5$ copies of $C_5$ ?proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#57	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#58	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#59	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	No formal statement	No Result decision
#60	Does every graph on $n$ vertices with $>\mathrm{ex}(n;C_4)$ edges contain $\gg n^{1/2}$ many copies of $C_4$ ?openFormalized	open	In Lean	No Result decision
#61	The Erdős–Hajnal Conjecture states that there is a constant $c(H) > 0$ for each $H$ such that we can take $f(n) = n^{c(H)}$ in the above formulation.openFormalized	open	In Lean	No Result decision
#62	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#63	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#64	Does every finite graph with minimum degree at least $3$ contain a cycle of length $2^k$ for some $k \geq 2$ ?falsifiableFormalized	falsifiable	In Lean	No Result decision
#65	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#70	Erdős Problem 70: Let $\mathfrak{c}$ be the cardinality of the continuum, let $\beta$ be a countable ordinal, and let $2 \le n < \omega$ . Is it true that $\mathfrak{c} \to (\beta, n)^3_2$ ?openFormalized	open	In Lean	No Result decision
#71	Is it true that for every infinite arithmetic progression $P$ which contains even numbers there is some constant $c=c(P)$ such that every graph with average degree at least $c$ contains a cycle whose length is in $P$ ?proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#72	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#73	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#74	Let $f(n)\to \infty$ possibly very slowly. Is there a graph of infinite chromatic number such that every finite subgraph on $n$ vertices can be made bipartite by deleting at most $f(n)$ edges?openFormalized	open	In Lean	No Result decision
#75	Is there a graph of chromatic number `ℵ_ 1` with `ℵ_ 1` vertices such that for all `ε > 0`, if `n` is sufficiently large and `H` is a subgraph on `n` vertices, then `H` contains an independent set of size `> n ^ (1 - ε)`?openFormalized	open	In Lean	No Result decision
#76	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#77	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#78	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#79	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#80	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#81	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#82	$F(n) / \log n \to \infty as n \to \infty$ openFormalized	open	In Lean	No Result decision
#84	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#85	Is it true that, for all large $n$ , $f(n + 1) \ge f(n)$ ?openFormalized	open	In Lean	No Result decision
#86	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#87	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#88	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#108	For every r ≥ 4 and k ≥ 2 is there some finite f(k,r) such that every graph of chromatic number ≥ f(k,r) contains a subgraph of girth ≥ r and chromatic number ≥ k?openFormalized	open	In Lean	No Result decision
#110	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	No formal statement	No Result decision
#111	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#112	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#113	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	No formal statement	No Result decision
#127	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#128	Let G be a graph with n vertices such that every induced subgraph on ≥ $n/2$ vertices has more than $n^2/50$ edges. Must G contain a triangle?falsifiableFormalized	falsifiable	In Lean	No Result decision
#129	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#130	Let $A\subset\mathbb{R}^2$ be an infinite set which contains no three points on a line and no four points on a circle. Consider the graph with vertices the points in $A$ , where two vertices are joined by an edge if and only if they are an integer distance apart. How large can the chromatic number and clique number of this graph be? In particular, can the chromatic number be infinite?openFormalized	open	In Lean	No Result decision
#133	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	No formal statement	No Result decision
#134	Let $\epsilon,\delta>0$ and $n$ be sufficiently large in terms of $\epsilon$ and $\delta$ . Let $G$ be a triangle-free graph on $n$ vertices with maximum degree $<n^{1/2-\epsilon}$ . Can $G$ be made into a triangle-free graph with diameter $2$ by adding at most $\delta n^2$ edges?proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#136	No statement retained — open to read what the source holdssolvedNo formal declaration	solved	No formal statement	No Result decision
#146	If $H$ is bipartite and is $r$ -degenerate, that is, every induced subgraph of $H$ has minimum degree $\leq r$ , then $\mathrm{ex}(n;H) \ll n^{2-1/r}.$ open (Lean)Formalized	open (Lean)	In Lean	No Result decision
#147	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	No formal statement	No Result decision
#149	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#150	A minimal cut of a graph is a minimal set of vertices whose removal disconnects the graph. Let $c(n)$ be the maximum number of minimal cuts a graph on $n$ vertices can have.proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#151	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision

Problems

Search problems.science