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

Full distribution

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

22 Problems

Number	Question	Source says	Formal	Result here
#57	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#58	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	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$ ?Source says openFormalized	open	In Lean	No Result decision
#63	No statement retained — open to read what the source holdsSource says provedNo 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$ ?Source says falsifiableFormalized	falsifiable	In Lean	No Result decision
#65	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	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$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#72	No statement retained — open to read what the source holdsSource says provedNo 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?Source says openFormalized	open	In Lean	No Result decision
#84	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	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?Source says openFormalized	open	In Lean	No Result decision
#110	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#184	Any graph on $n$ vertices can be decomposed into $O(n)$ many edge-disjoint cycles and edges.Source says openFormalized	open	In Lean	No Result decision
#584	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#585	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#626	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#642	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#752	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#916	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#921	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#1006	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#1016	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision