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

102 Problems

2/3

Number	Question	Source says	Formal	Result here
#484	Prove that there exists an absolute constant $c>0$ such that, whenever $\{1,\ldots,N\}$ is $k$ -coloured (and $N$ is large enough depending on $k$ ) then there are at least $cN$ many integers in $\{1,\ldots,N\}$ which are representable as a monochromatic sum (that is, $a+b$ where $a,b\in \{1,\ldots,N\}$ are in the same colour class and $a\neq b$ ).Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#494	Selfridge and Straus [SeSt58] proved that $A$ is determined by $A_k$ if $\|A\|$ is divisible by a prime greater than $k$ .Source says provedFormalized	proved	In Lean	No Result decision
#645	If ℕ is $2$ -coloured then there must exist a monochromatic three-term arithmetic progression $x,x+d,x+2d$ such that $d>x$ .Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#656	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#658	No statement retained — open to read what the source holdsSource says proved (Lean)No formal declaration	proved (Lean)	No formal statement	No Result decision
#707	Erdős Problem 707: It is false that any finite Sidon set can be embedded in a perfect different set modulo some $n$ .Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#721	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#741	Let $A\subseteq \mathbb{N}$ be such that $A+A$ has positive upper density. Can one always decompose $A=A_1\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive upper density?Source says solved (Lean)Formalized	solved (Lean)	In Lean	No Result decision
#749	Let $\epsilon>0$ . Does there exist $A\subseteq \mathbb{N}$ such that the lower density of $A+A$ is at least $1-\epsilon$ and yet $1_A\ast 1_A(n) \ll_\epsilon 1$ for all $n$ ?Source says openFormalized	open	In Lean	No Result decision
#763	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#764	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#772	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#781	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#785	Let $A,B\subseteq \mathbb{N}$ be infinite sets such that $A+B$ contains all large integers. Let $A(x)=\lvert A\cap [1,x]\rvert$ and similarly for $B(x)$ . Is it true that if $A(x)B(x)\sim x$ then $A(x)B(x)-x\to \infty$ as $x\to \infty$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#787	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#788	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#789	Let $h(n)$ be maximal such that if $A\subseteq \mathbb{Z}$ with $\lvert A\rvert=n$ then there is $B\subseteq A$ with $\lvert B\rvert \geq h(n)$ such that if $a_1+\cdots+a_r=b_1+\cdots+b_s$ with $a_i,b_i\in B$ then $r=s$ .Source says openFormalized	open	In Lean	No Result decision
#790	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#791	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#792	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#806	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#808	No statement retained — open to read what the source holdsSource says disprovedNo formal declaration	disproved	No formal statement	No Result decision
#817	Let $k \geq 3$ . Define $g_k(n)$ to be the minimal $N$ such that $\{1, ..., N\}$ contains some $A$ of size $\|A\| = n$ such that $\langle A\rangle = \left\{\sum_{a \in A} \epsilon_a a : \epsilon_a \in\{0, 1\}\right\}$ contains no non-trivial $k$ -term arithmetic progression. Estimate $g_k(n)$ . In particular, is it true that $g_3(n) \gg 3^n$ Source says openFormalized	open	In Lean	No Result decision
#818	Let $A$ be a finite set of integers such that $\lvert A+A\rvert \ll \lvert A\rvert$ . Is it true that $\lvert AA\rvert \gg \frac{\lvert A\rvert^2}{(\log \lvert A\rvert)^C}$ for some constant $C>0$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#819	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#840	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#847	Let $A \subset \mathbb{N}$ be an infinite set for which there exists some $\epsilon > 0$ such that in any subset of $A$ of size $n$ there is a subset of size at least $\epsilon n$ which contains no three-term arithmetic progression.Source says disprovedFormalized	disproved	In Lean	No Result decision
#863	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#864	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#865	There exists a constant $C>0$ such that, for all large $N$ , if $A\subseteq \{1,\ldots,N\}$ has size at least $\frac{5}{8}N+C$ then there are distinct $a,b,c\in A$ such that $a+b,a+c,b+c\in A$ .Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#866	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#867	Is it true that if $A=\{a_1<\cdots <a_t\}\subseteq \{1,\ldots,N\}$ has no solutions to $a_i+a_{i+1}+\cdots+a_j\in A$ then $\lvert A\rvert \leq \frac{N}{2}+O(1)?$ Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#874	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#875	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#876	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#877	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#895	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#899	Let $A\subseteq\mathbb{N}$ be an infinite set such that $\|A\cap \{1, ..., N\}\| = o(N)$ . Is it true that $\limsup_{N\to\infty}\frac{\|(A - A)\cap \{1, ..., N\}\|}{\|A \cap \{1, ..., N\}\|} = \infty?$ Source says provedFormalized	proved	In Lean	No Result decision
#966	Let $k,r\geq 2$ . Does there exist a set $A\subseteq \mathbb{N}$ that contains no non-trivial arithmetic progression of length $k+1$ , yet in any $r$ -colouring of $A$ there must exist a monochromatic non-trivial arithmetic progression of length $k$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#984	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#1097	The main conjecture: for any finite set of integers $A$ with $\|A\| = n$ , the number of distinct common differences in three-term arithmetic progressions is $O(n^{3/2})$ .Source says openFormalized	open	In Lean	No Result decision
#1112	No statement retained — open to read what the source holdsSource says open (Lean)No formal declaration	open (Lean)	No formal statement	No Result decision
#1145	Let $A=\{1\leq a_1 < a_2 < \cdots\}$ and $B=\{1\leq b_1 < b_2 < \cdots\}$ be sets of integers with $a_n/b_n\to 1$ .Source says openFormalized	open	In Lean	No Result decision
#1179	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#1185	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#1186	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1187	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#1191	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision