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
#114	No statement retained — open to read what the source holdsSource says falsifiableNo formal declaration	falsifiable	No formal statement	No Result decision
#115	If $p(z)$ is a polynomial of degree $n$ such that $\{z : \lvert p(z)\rvert\leq 1\}$ is connected then is it true that $\max_{\substack{z\in\mathbb{C}\\ \lvert p(z)\rvert\leq 1}} \lvert p'(z)\rvert \leq (\tfrac{1}{2}+o(1))n^2?$ Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#116	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#119	Is it true that $\limsup M_n = \infty$ ?Source says solvedFormalized	solved	In Lean	No Result decision
#228	Does there exist, for all large $n$ , a polynomial $P$ of degree $n$ , with coefficients $\pm1$ , such that $\sqrt n \ll \|P(z)\| \ll \sqrt n$ for all $\|z\|=1$ , with the implied constants independent of $z$ and $n$ ?Source says provedFormalized	proved	In Lean	No Result decision
#230	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#485	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#521	Let $(\epsilon_k)_{k\geq 0}$ be independently uniformly chosen at random from $\{-1,1\}$ . If $R_n$ counts the number of real roots of $f_n(z)=\sum_{0\leq k\leq n}\epsilon_k z^k$ then is it true that, almost surely, $\lim_{n\to \infty}\frac{R_n}{\log n}=\frac{2}{\pi}?$ Source says openFormalized	open	In Lean	No Result decision
#522	Let $f(z)=\sum_{0\leq k\leq n} \epsilon_k z^k$ be a random polynomial, where $\epsilon_k\in \{-1,1\}$ independently uniformly at random for $0\leq k\leq n$ .Source says openFormalized	open	In Lean	No Result decision
#523	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#524	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#525	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	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
#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