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

1,217 Problems · 2 with reviewed evidence

17/26

Number	Question	Source says	Formal	Result here
#769	Let $c(n)$ be minimal such that if $k\geq c(n)$ then the $n$ -dimensional unit cube can be decomposed into $k$ homothetic $n$ -dimensional cubes. Give good bounds for $c(n)$ — in particular, is it true that $c(n)\gg n^n$ ?openFormalized	open	In Lean	No Result decision
#770	`n + 1` is prime iff `h n = n + 1`. This is described as 'easy to see' in [Er74b].openFormalized	open	In Lean	No Result decision
#771	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#772	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#773	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#774	Is every proportionately dissociated (infinite) set the union of a finite number of dissociated sets?openFormalized	open	In Lean	No Result decision
#775	Is there a $3$ -uniform hypergraph on $n$ vertices which contains at least $n-O(1)$ different sizes of cliques (maximal complete subgraphs)?disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#776	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#777	No statement retained — open to read what the source holdssolvedNo formal declaration	solved	No formal statement	No Result decision
#778	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#779	A Conjecture of Marian Deaconescu, see p.120 in https://doi.org/10.2307/2975810falsifiableFormalized	falsifiable	In Lean	No Result decision
#780	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#781	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	No formal statement	No Result decision
#782	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#783	No statement retained — open to read what the source holdssolvedNo formal declaration	solved	No formal statement	No Result decision
#784	No statement retained — open to read what the source holdssolvedNo formal declaration	solved	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$ ?proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#786	Let $\epsilon > 0$ . Is there some set $A\subset\mathbb{N}$ of density $> 1 - \epsilon$ such that $a_1\cdots a_r = b_1\cdots b_s$ with $a_i, b_j\in A$ can only hold when $r = s$ ?openFormalized	open	In Lean	No Result decision
#787	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#788	No statement retained — open to read what the source holdsopenNo 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$ .openFormalized	open	In Lean	No Result decision
#790	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#791	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#792	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#793	No statement retained — open to read what the source holdsproved (Lean)No formal declaration	proved (Lean)	No formal statement	No Result decision
#794	Is it true that every $3$ -uniform hypergraph on $3n$ vertices with at least $n^3+1$ edges must contain either a subgraph on $4$ vertices with $3$ edges or a subgraph on $5$ vertices with $7$ edges?disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#795	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#796	Let $k\geq 2$ and let $g_k(n)$ be the largest possible size of $A\subseteq \{1,\ldots,n\}$ such that every $m$ has $<k$ solutions to $m=a_1a_2$ with $a_1<a_2\in A$ . Is it true that $g_3(n)=\frac{\log\log n}{\log n}n+(c+o(1))\frac{n}{\log n}$ for some constant $c$ ?openFormalized	open	In Lean	No Result decision
#797	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#798	Let $t(n)$ be the minimum number of points in $\{1,\ldots,n\}^2$ such that the $\binom{t}{2}$ lines determined by these points cover all points in $\{1,\ldots,n\}^2$ .proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#799	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#800	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#801	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#802	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#803	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	No formal statement	No Result decision
#804	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	No formal statement	No Result decision
#805	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#806	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#807	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	No formal statement	No Result decision
#808	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	No formal statement	No Result decision
#809	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#810	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#811	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#812	Is it true that $\frac{R(n+1)}{R(n)}\geq 1+c$ for some constant $c>0$ , for all large $n$ ?openFormalized	open	In Lean	No Result decision
#813	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#814	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#815	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	No formal statement	No Result decision
#816	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision

Problems

Search problems.science