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

61 Problems

2/2

Number	Question	Source says	Formal	Result here
#1059	Are there infinitely many primes $p$ such that $p - k!$ is composite for each $k$ such that $1 ≤ k! < p$ ?Source says openFormalized	open	In Lean	No Result decision
#1137	Let $d_n=p_{n+1}-p_n$ , where $p_n$ denotes the $n$ th prime. Is it true that $\frac{\max_{n < x}d_{n}d_{n-1}}{(\max_{n < x}d_n)^2}\to 0$ as $x\to \infty$ ?Source says openFormalized	open	In Lean	No Result decision
#1138	Erdős Problem 1138. Let $x/2 < y < x$ and $C > 1$ . If $d = \max_{p_n < x}(p_{n+1} - p_n)$ , where $p_n$ denotes the $n$ -th prime, then is it true that $\pi(y + Cd) - \pi(y) \sim \frac{Cd}{\log y}$ ?Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#1139	Let $1\leq u_1 < u_2 < \cdots$ be the sequence of integers with at most $2$ prime factors. Is it true that $\limsup_{k \to \infty} \frac{u_{k+1}-u_k}{\log k}=\infty?$ Source says openFormalized	open	In Lean	No Result decision
#1141	Are there infinitely many $n$ such that $n-k^2$ is prime for all $k$ with $(n,k)=1$ and $k^2 < n$ ?Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#1142	Are there infinitely many $n > 2$ such that $n - 2^k$ is prime for all $k \geq 1$ with $2^k < n$ ?Source says openFormalized	open	In Lean	No Result decision
#1143	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1184	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
#1200	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#1201	Is it true that for every $\epsilon,\eta>0$ there exists a $k$ such that the density of $n$ for which $P(n(n+1)\cdots(n+k))>n^{1-\epsilon}$ is at least $1-\eta$ (where $P(m)$ is the greatest prime divisor of $m$ )?Source says openFormalized	open	In Lean	No Result decision
#1202	No statement retained — open to read what the source holdsSource says solvedNo formal declaration	solved	No formal statement	No Result decision
#1212	Roughness criterion (sufficiency for the anchor conditions): if $a < s$ for all $s$ in the leg and the leg stays below $a + P^-(a)$ , then $a$ is coprime to the whole leg. Stated via divisibility: no prime factor of $a$ divides any $s$ with $a < s < a + p$ for all prime factors $p$ of $a$ .Source says openFormalized	open	In Lean	No Result decision