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

79 Problems

2/2

Number	Question	Source says	Formal	Result here
#1039	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1040	No statement retained — open to read what the source holdsopenNo 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$ .falsifiableFormalized	falsifiable	In Lean	No Result decision
#1042	No statement retained — open to read what the source holdsprovedNo 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$ ?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)$ .solved (Lean)Formalized	solved (Lean)	In Lean	No Result decision
#1045	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1046	No statement retained — open to read what the source holdsdisprovedNo 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.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$ ?disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#1114	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#1115	No statement retained — open to read what the source holdssolvedNo formal declaration	solved	No formal statement	No Result decision
#1116	No statement retained — open to read what the source holdssolvedNo formal declaration	solved	No formal statement	No Result decision
#1117	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1118	No statement retained — open to read what the source holdssolvedNo 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}$ ?independentFormalized	independent	In Lean	No Result decision
#1120	No statement retained — open to read what the source holdsopenNo 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?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$ .proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#1129	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#1130	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#1131	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1132	No statement retained — open to read what the source holdsopenNo 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.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}?$ openFormalized	open	In Lean	No Result decision
#1151	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1152	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#1153	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#1154	No statement retained — open to read what the source holdsnot disprovableNo formal declaration	not disprovable	No formal statement	No Result decision
#1197	No statement retained — open to read what the source holdsdisproved (Lean)No formal declaration	disproved (Lean)	No formal statement	No Result decision
#1215	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	No formal statement	No Result decision

Problems

Search problems.science