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

22 Problems

Number	Question	Source says	Formal	Result here
#175	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#376	Are there infinitely many $n$ such that ${2n\choose n}$ is coprime to $105$ ?Source says openFormalized	open	In Lean	No Result decision
#377	Is there some absolute constant $C > 0$ such that $\sum_{p \leq n} 1_{p\nmid {2n \choose n}}\frac{1}{p} \leq C$ for all $n$ ?Source says openFormalized	open	In Lean	No Result decision
#378	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#379	Let $S(n)$ denote the largest integer such that, for all $1 ≤ k < n$ , the binomial coefficient $\binom{n}{k}$ is divisible by $p^S(n)$ for some prime $p$ (depending on $k$ ).Then $\limsup S(n) = \infty$ .Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#384	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#386	There is a $k$ , such that $2 \le k \le n - 2$ and $\binom{n}{k}$ can be the product of consecutive primes infinitely often?Source says openFormalized	open	In Lean	No Result decision
#387	Is there an absolute constant $c > 0$ such that, for all $1 \leq k < n$ , the binomial coefficient $\binom{n}{k}$ has a divisor in $(cn, n]$ ?Source says solvedFormalized	solved	In Lean	No Result decision
#396	Is it true that for every $k$ there exists $n$ such that $\prod_{0\leq i\leq k}(n-i) \mid \binom{2n}{n}?$ Source says openFormalized	open	In Lean	No Result decision
#397	Are there only finitely many solutions to $\prod_i \binom{2m_i}{m_i}=\prod_j \binom{2n_j}{n_j}$ with the $m_i,n_j$ distinct?Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#683	There exists $c > 0$ such that $P(n, k) > \min\{n-k+1, k^{1 + c}\}$ for all $0 < k < n$ .}Source says openFormalized	open	In Lean	No Result decision
#684	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#685	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#698	Is there some $h(n)\to \infty$ such that for all $2\leq i<j\leq n/2$ $\textrm{gcd}\left( \binom{n}{i},\binom{n}{j}\right) \geq h(n)?$ Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#699	Erdős Problem 699. Is it true that for every $1 \le i < j \le n / 2$ there exists a prime $p \ge i$ with $p \mid \gcd\big(\binom{n}{i}, \binom{n}{j}\big)$ ?Source says falsifiableFormalized	falsifiable	In Lean	No Result decision
#700	`f n` unfolds to the infimum of `fSet n`.Source says openFormalized	open	In Lean	No Result decision
#730	Are there infinitely many pairs of integers $n < m$ such that $\binom{2n}{n}$ and $\binom{2m}{m}$ have the same set of prime divisors?Source says openFormalized	open	In Lean	No Result decision
#731	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#849	Is it true that, for every integer $t\geq1$ , there is some integer $a$ such that ${n \choose k} = a$ with $1\leq k \le \frac{n}{2}$ has exactly $t$ solutions?Source says openFormalized	open	In Lean	No Result decision
#1093	Are there infinitely many binomial coefficients with deficiency 1?Source says openFormalized	open	In Lean	No Result decision
#1094	For all $n\ge 2k$ the least prime factor of $\binom{n}{k}$ is $\le\max(n/k,k)$ , with only finitely many exceptions.Source says openFormalized	open	In Lean	No Result decision
#1095	Sorenson, Sorenson, and Webster [SSWE20] give heuristic evidence that $\log g(k) \asymp \frac{k}{\log k}$ .Source says openFormalized	open	In Lean	No Result decision