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

79 Problems

2/2

Number	Question	Source says	Formal	Result here
#1039	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1040	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1041	Let $f(z) = \prod_{i=1}^{n} (z - z_i) \in \mathbb{C}[x]$ with $\|z_i\| < 1$ for all $i$ .Source says falsifiableFormalized	falsifiable	In Lean	No Result decision
#1042	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#1043	Erdős Problem 1043: Let $f\in \mathbb{C}[x]$ be a monic polynomial. Must there exist a straight line $\ell$ such that the projection of $\{ z: \lvert f(z)\rvert\leq 1\}$ onto $\ell$ has measure at most $2$ ?Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#1044	Let $f(z)=\prod_{i=1}^n(z-z_i)\in\mathbb{C}[x]$ where $\lvert z_i\rvert\leq 1$ for all $i$ . If $\Lambda(f)$ is the maximum of the lengths of the boundaries of the connected components of $\{ z: \lvert f(z)\rvert<1\}$ then determine the infimum of $\Lambda(f)$ .Source says solved (Lean)Formalized	solved (Lean)	In Lean	No Result decision
#1045	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1046	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#1047	Let $f\in \mathbb{C}[x]$ be a monic polynomial with $m$ distinct roots, and let $c>0$ be a constant small enough such that $\{ z: \lvert f(z)\rvert\leq c\}$ has $m$ distinct connected components.Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#1048	If $f\in \mathbb{C}[x]$ is a monic polynomial with all roots satisfying $\lvert z\rvert \leq r$ for some $r<2$ , then must $\{ z: \lvert f(z)\rvert <1\}$ have a connected component with diameter $>2-r$ ?Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#1114	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#1115	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#1116	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#1117	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1118	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#1119	Let $\mathfrak{m}$ be an infinite cardinal with $\aleph_0 < \mathfrak{m} < \mathfrak{c} = 2^{\aleph_0}$ . Let $\{f_\alpha\}$ be a family of entire functions such that, for every $z_0 \in \mathbb{C}$ , there are at most $\mathfrak{m}$ distinct values of $f_\alpha(z_0)$ . Must $\{f_\alpha\}$ have cardinality at most $\mathfrak{m}$ ?Source says independentFormalized	independent	In Lean	No Result decision
#1120	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1125	Let $f:\mathbb{R}\to \mathbb{R}$ be such that $2f(x) \leq f(x+h)+f(x+2h)$ for every $x\in \mathbb{R}$ and $h>0$ . Must $f$ be monotonic?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#1126	If $f(x+y)=f(x)+f(y)$ for almost all $x,y\in \mathbb{R}$ then there exists a function $g$ such that $g(x+y)=g(x)+g(y)$ for all $x,y\in\mathbb{R}$ such that $f(x)=g(x)$ for almost all $x$ .Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#1129	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#1130	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#1131	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1132	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1133	Let $C>0$ . There exists $\epsilon>0$ such that if $n$ is sufficiently large the following holds.Source says openFormalized	open	In Lean	No Result decision
#1150	Is there some constant $c > 0$ such that, for all large enough $n$ and all polynomials $P$ of degree $n$ with coefficients in $\{-1, 1\}$ , $\max_{\|z\|=1} \|P(z)\| > (1 + c) \sqrt{n}?$ Source says openFormalized	open	In Lean	No Result decision
#1151	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1152	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1153	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#1154	No statement retained — open to read what the source holdsSource says not disprovableNo formal declaration	not disprovable	No formal statement	No Result decision
#1197	No statement retained — open to read what the source holdsSource says disproved (Lean)No formal declaration	disproved (Lean)	No formal statement	No Result decision
#1215	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision