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

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$ .openFormalized	open	In Lean	No Result decision
#1085	Erdős showed $f_2(n) > n^{1+c/\log\log n}$ for some $c > 0$ .openFormalized	open	In Lean	No Result decision
#1086	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1087	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1088	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1089	No statement retained — open to read what the source holdssolvedNo 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?proved (Lean)Formalized	proved (Lean)	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
#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$ .proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#1124	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#1127	No statement retained — open to read what the source holdsindependentNo formal declaration	independent	No formal statement	No Result decision
#1207	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1208	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision

Problems

Search problems.science