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

20/26

Number	Question	Source says	Formal	Result here
#913	Are there infinitely many $n$ such that if $n(n + 1) = \prod_i p_i^{k_i}$ is the factorisation into distinct primes then all exponents $k_i$ are distinct?openFormalized	open	In Lean	No Result decision
#914	Let $r\geq 2$ and $m\geq 1$ . Every graph with $rm$ vertices and minimum degree at least $m(r-1)$ contains $m$ vertex disjoint copies of $K_r$ .proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#915	No statement retained — open to read what the source holdssolvedNo formal declaration	solved	No formal statement	No Result decision
#916	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#917	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#918	Is there a graph with $\aleph_2$ vertices and chromatic number $\aleph_2$ such that every subgraph on $\aleph_1$ vertices has chromatic number $\leq\aleph_0$ ?openFormalized	open	In Lean	No Result decision
#919	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#920	Is it true that, for $k\geq 4$ , $f_k(n) \gg \frac{n^{1-\frac{1}{k-1}}}{(\log n)^{c_k}}$ for some constant $c_k>0$ ?solvedFormalized	solved	In Lean	No Result decision
#921	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#922	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#923	Is it true that, for every $k$ , there is some $f(k)$ such that if $G$ has chromatic number $\geq f(k)$ then $G$ contains a triangle-free subgraph with chromatic number $\geq k$ ?proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#924	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#925	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	No formal statement	No Result decision
#926	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#927	No statement retained — open to read what the source holdsdisproved (Lean)No formal declaration	disproved (Lean)	No formal statement	No Result decision
#928	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#929	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#930	Is it true that, for every $r$ , there is a $k$ such that if $I_1,\ldots,I_r$ are disjoint intervals of consecutive integers, all of length at least $k$ , then $\prod_{1\leq i\leq r}\prod_{m\in I_i}m$ is not a perfect power?openFormalized	open	In Lean	No Result decision
#931	Let $k_1 \geq k_2 \geq 3$ . Are there only finitely many $n_2\geq n_1 + k_1$ such that $\prod_{1\leq i\leq k_1}(n_1 + i)\ \text{and}\ \prod_{1\leq j\leq k_2} (n_2 + j)$ have the same prime factors?openFormalized	open	In Lean	No Result decision
#932	Let $p_k$ denote the $k$ th prime. For infinitely many $r$ there are at least two integers $p_r < n < p_{r+1}$ all of whose prime factors are $< p_{r + 1} - p_r$ .openFormalized	open	In Lean	No Result decision
#933	If $n(n+1)=2^k3^lm$ , where $(m,6)=1$ , then is it true that $\limsup_{n\to \infty} \frac{2^k3^l}{n\log n}=\infty$ ?openFormalized	open	In Lean	No Result decision
#934	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#935	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#936	Is $n! + 1$ powerful for finitely many $n$ ?openFormalized	open	In Lean	No Result decision
#937	Are there infinitely many four-term arithmetic progressions of coprime powerful numbers? (A number $n$ is powerful if $p \mid n \to p^2 \mid n$ ; `Nat.Powerful`.)provedFormalized	proved	In Lean	No Result decision
#938	Let $A=\{n_1 < n_2 < \cdots\}$ be the sequence of powerful numbers (if $p\mid n$ then $p^2\mid n$ ). Are there only finitely many three-term progressions of consecutive terms $n_k,n_{k+1},n_{k+2}$ ?openFormalized	open	In Lean	No Result decision
#939	If $r≥4$ then can the sum of $r-2$ coprime $r$ -powerful numbers ever be itself $r$ -powerful?openFormalized	open	In Lean	No Result decision
#940	Let $r \ge 3$ . Is it true that the set of integers which are the sum of at most $r$ $r$ -powerful numbers has density $0$ ?openFormalized	open	In Lean	No Result decision
#941	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#942	Is there some constant $c > 0$ such that $h(n) < (\log n)^{c + o(1)}$ and, for infinitely many $n$ , $h(n) > (\log n)^{c - o(1)}$ .openFormalized	open	In Lean	No Result decision
#943	Let $A$ be the set of powerful numbers. Is is true that $1_A\ast 1_A(n)=n^{o(1)}$ for every $n$ ?openFormalized	open	In Lean	No Result decision
#944	Let $k \ge 4$ and $r\ge 1$ . Must there exist a graph $G$ with chromatic number $k$ such that every vertex is critical, yet every critical set of edges has size $>r$ ?openFormalized	open	In Lean	No Result decision
#945	Is it true that $F(x) \leq (\log x)^{O(1)}$ ?openFormalized	open	In Lean	No Result decision
#946	There are infinitely many $n$ such that $τ(n) = τ(n+1)$ . Proved in [He84]. Here τ is the divisor counting function, which is `σ 0` in mathlib.provedFormalized	proved	In Lean	No Result decision
#947	No statement retained — open to read what the source holdsproved (Lean)No formal declaration	proved (Lean)	No formal statement	No Result decision
#948	No statement retained — open to read what the source holdssolvedNo formal declaration	solved	No formal statement	No Result decision
#949	Let $S \subseteq \mathbb{R}$ be a set containing no solutions to $a + b = c$ . Must there be a set $A \subseteq \mathbb{R} \setminus S$ of cardinality continuum such that $A + A \subseteq \mathbb{R}\setminus S$ ?openFormalized	open	In Lean	No Result decision
#950	Is it true that $\liminf f(n)=1$ ?openFormalized	open	In Lean	No Result decision
#951	If `1 < a 0 < ...` has property `Erdos951Prop`, is it true that `#{a i ≤ x} ≤ π x`?openFormalized	open	In Lean	No Result decision
#952	Is there an infinite sequence of distinct Gaussian primes $x_1,x_2,\ldots$ such that $\lvert x_{n+1}-x_n\rvert \ll 1$ ?openFormalized	open	In Lean	No Result decision
#953	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#954	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#955	If $A\subset \mathbb{N}$ has density $0$ then $s^{-1}(A)$ must also have density $0$ .openFormalized	open	In Lean	No Result decision
#956	No statement retained — open to read what the source holdsopenNo formal declaration	open	No formal statement	No Result decision
#957	No statement retained — open to read what the source holdsprovedNo formal declaration	proved	No formal statement	No Result decision
#958	Let $A\subset \mathbb{R}^2$ be a finite set of size $n$ , and let $\{d_1,\ldots,d_k\}$ be the set of distances determined by $A$ . Let $f(d)$ be the multiplicity of $d$ , that is, the number of unordered pairs from $A$ of distance $d$ apart.disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#959	Let $A\subseteq \mathbb{R}^2$ be a set of size $n$ and let $\{d_1,\ldots,d_k\}$ be the set of distinct distances determined by $A$ . Let $f(d)$ be the number of times the distance $d$ is determined, ordered so that $f(d_1)\geq f(d_2)\geq \cdots \geq f(d_k)$ . Estimate $\max (f(d_1)-f(d_2)),$ where the maximum is taken over all $A$ of size $n$ (this is `extremalGap n`).openFormalized	open	In Lean	No Result decision
#960	No statement retained — open to read what the source holdsdisprovedNo formal declaration	disproved	No formal statement	No Result decision

Problems

Search problems.science