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

110 Problems · 1 with reviewed evidence

3/3

Number	Question	Source says	Formal	Result here
#1084	It is easy to check that $f_2(n) < 3n$ .Source says openFormalized	open	In Lean	No Result decision
#1085	Erdős showed $f_2(n) > n^{1+c/\log\log n}$ for some $c > 0$ .Source says openFormalized	open	In Lean	No Result decision
#1086	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1087	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1088	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1089	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#1090	Let $k\geq 3$ . Does there exist a finite set $A\subset \mathbb{R}^2$ such that, in any $2$ -colouring of $A$ , there exists a line which contains at least $k$ points from $A$ , and all the points of $A$ on the line have the same colour?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#1091	No statement retained — open to read what the source holdsSource says solvedNo 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.Source says disprovedFormalized	disproved	In Lean	No Result decision
#1121	If $C_1,\ldots,C_n$ are circles in $\mathbb{R}^2$ with radii $r_1,\ldots,r_n$ such that no line disjoint from all the circles divides them into two non-empty sets then the circles can be covered by a circle of radius $r=\sum r_i$ .Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#1124	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#1127	No statement retained — open to read what the source holdsSource says independentNo formal declaration	independent	No formal statement	No Result decision
#1207	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1208	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision