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

47 Problems

Number	Question	Source says	Formal	Result here
#20	Is it true that $f(n,k) < c_k^n$ for some constant $c_k>0$ and for all $n > 0$ ?Source says openFormalized	open	In Lean	No Result decision
#21	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#83	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#120	Let $A \subseteq \mathbb{R}$ be an infinite set. Must there be a set $E \subseteq \mathbb{R}$ of positive measure which does not contain any set of the shape $a * A + b$ for some $a,b \in \mathbb{R}$ and $a \neq 0$ ?Source says openFormalized	open	In Lean	No Result decision
#161	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#162	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#171	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#191	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#192	No statement retained — open to read what the source holdsSource says solved (Lean)No formal declaration	solved (Lean)	No formal statement	No Result decision
#207	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#231	No statement retained — open to read what the source holdsSource says disproved (Lean)No formal declaration	disproved (Lean)	No formal statement	No Result decision
#447	How large can a union-free collection $\mathcal{F}$ of subsets of $[n]$ be? By union-free we mean there are no solutions to $A\cup B=C$ with distinct $A,B,C\in \mathcal{F}$ . Must $\lvert \mathcal{F}\rvert =o(2^n)$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#497	How many antichains in $[n]$ are there? That is, how many families of subsets of $[n]$ are there such that, if $\mathcal{F}$ is such a family and $A,B\in \mathcal{F}$ , then $A\not\subseteq B$ ?Source says solved (Lean)Formalized	solved (Lean)	In Lean	No Result decision
#498	Let $z_1,\ldots,z_n\in\mathbb{C}$ with $1\leq \lvert z_i\rvert$ for $1\leq i\leq n$ . Let $D$ be an arbitrary disc of radius $1$ . Is it true that the number of sums of the shape $\sum_{i=1}^n\epsilon_iz_i \textrm{ for }\epsilon_i\in \{-1,1\}$ which lie in $D$ is at most $\binom{n}{\lfloor n/2\rfloor}$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#499	Let $M$ be a real $n \times n$ doubly stochastic matrix. Does there exist some $σ \in S_n$ such that $\prod_{1 \leq i \leq n} M_{i, σ(i)} \geq n^{-n}?$ This is true, and was proved by Marcus and Minc [MaMi62]Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#501	For every $x \in \mathbb{R}$ let $A_x \subset \mathbb{R}$ be a bounded set with outer measure $< 1$ . Must there exist an infinite independent set, that is, some infinite $X \subseteq \mathbb{R}$ such that $x \notin A_y$ for all $x \neq y \in X$ ?Source says openFormalized	open	In Lean	No Result decision
#602	Does every almost-disjoint family of countably infinite sets whose pairwise intersections all have size ≠ 1 have Property B?Source says openFormalized	open	In Lean	No Result decision
#603	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#624	Let $X$ be a finite set of size $n$ and $H(n)$ be such that there is a function $f:\{A : A\subseteq X\}\to X$ so that for every $Y\subseteq X$ with $\lvert Y\rvert \geq H(n)$ we have $\left\{ f(A) : A\subseteq Y\right\}=X$ . Prove that $H(n)-\log_2 n \to \infty$ .Source says openFormalized	open	In Lean	No Result decision
#644	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#664	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#665	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#701	Let $\mathcal{F}$ be a family of sets closed under taking subsets (i.e. if $B\subseteq A\in\mathcal{F}$ then $B\in \mathcal{F}$ ). There exists some element $x$ such that whenever $\mathcal{F}'\subseteq \mathcal{F}$ is an intersecting subfamily we have $\lvert \mathcal{F}'\rvert \leq \lvert \{ A\in \mathcal{F} : x\in A\}\rvert.$ Source says openFormalized	open	In Lean	No Result decision
#702	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#703	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#722	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#723	If there is a finite projective plane of order $n$ then must $n$ be a prime power?Source says falsifiableFormalized	falsifiable	In Lean	No Result decision
#724	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#725	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#732	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#733	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#734	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#747	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#776	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#777	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#780	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#857	Estimate `m(n,k)`, or better give an asymptotic formula.Source says openFormalized	open	In Lean	No Result decision
#901	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#903	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#1022	Is there a constant $c_t$ , where $c_t\to \infty$ as $t\to \infty$ , such that if $\mathcal{F}$ is a finite family of finite sets, all of size at least $t$ , and for every set $X$ there are $<c_t\lvert X\rvert$ many $A\in \mathcal{F}$ with $A\subseteq X$ , then $\mathcal{F}$ has chromatic number $2$ (in other words, has property B)?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#1023	Let $F(n)$ be the maximal size of a family of subsets of $\{1,\ldots,n\}$ such that no set in this family is the union of other members of the family. Is it true that there is a constant $c>0$ such that $F(n)\sim c \frac{2^n}{n^{1/2}}?$ Source says solved (Lean)Formalized	solved (Lean)	In Lean	No Result decision
#1025	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#1026	Let $x_1,\ldots,x_n$ be a sequence of distinct real numbers. Determine $\max\left(\sum x_{i_r}\right),$ where the maximum is taken over all monotonic subsequences.Source says solved (Lean)Formalized	solved (Lean)	In Lean	No Result decision
#1027	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#1159	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1173	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1183	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision