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

21 Problems

Number	Question	Source says	Formal	Result here
#18	Erdős's Theorem. Erdős proved that $h(n!) < n$ for all $n \ge 1$ .Source says openFormalized	open	In Lean	No Result decision
#373	Show that the equation `n!=a_1!a_2!···a_k!`, with `n−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k`, has only finitely many solutions.Source says openFormalized	open	In Lean	No Result decision
#390	Does there exists a constant `c` such that `f n - 2 * n ~ c * (n / log n)`?Source says openFormalized	open	In Lean	No Result decision
#391	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#392	Let $A(n)$ denote the least value of $t$ such that $n! = a_1 \cdots a_t$ with $a_1 \leq \cdots \leq a_t\leq n^2$ . Then $A(n) = \frac{n}{2} - \frac{n}{2\log n} + o\left(\frac{n}{\log n}\right).$ Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#393	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#398	Brocard's Problem Does $n! + 1 = m^2$ have integer solutions other than $n = 4, 5, 7$ ?Source says falsifiableFormalized	falsifiable	In Lean	No Result decision
#399	Is it true that there are no solutions to `n! = x^k ± y^k` with `x,y,n ∈ ℕ`, `x*y > 1`, and `k > 2`?Source says disproved (Lean)Formalized	disproved (Lean)	In Lean	No Result decision
#400	Can one show that $\sum_{n\leq x}g_k(n) \sim c_k x\log x$ for some constant $c_k$ ?Source says openFormalized	open	In Lean	No Result decision
#401	Is there some function $f(r)$ such that $f(r)\to \infty$ as $r\to\infty$ , such that, for infinitely many $n$ , there exist $a_1,a_2$ with $a_1+a_2> n+f(r)\log n$ such that $a_1!a_2! \mid n!2^n3^n\cdots p_r^n$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#403	Does the equation $2^m=a_1!+\cdots+a_k!$ with $a_1<a_2<\cdots <a_k$ have only finitely many solutions?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#404	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#405	No statement retained — open to read what the source holdsSource says provedNo formal declaration	proved	No formal statement	No Result decision
#419	If $\tau(n)$ counts the number of divisors of $n$ , then what is the set of limit points of $\frac{\tau((n+1)!)}{\tau(n!)}?$ Source says solved (Lean)Formalized	solved (Lean)	In Lean	No Result decision
#478	No statement retained — open to read what the source holdsSource says openNo formal declaration	open	No formal statement	No Result decision
#646	Let $p_1,\ldots,p_k$ be distinct primes. Are there infinitely many $n$ such that $n!$ is divisible by an even power of each of the $p_i$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#727	Let $k ≥ 2$ . Does $((n+k)!)^2∣(2n)!$ hold for infinitely many $n$ ?Source says openFormalized	open	In Lean	No Result decision
#728	Let $\varepsilon$ be sufficiently small and $C, C' > 0$ . Are there integers $a, b, n$ such that $a, b > \varepsilon n\quad a!\, b! \mid n!\, (a + b - n)!,$ and $C \log n < a + b - n < C' \log n ?$ Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#729	Let $C>0$ be a constant. Are there infinitely many integers $a,b,n$ with $a+b> n+C\log n$ such that the denominator of $\frac{n!}{a!b!}$ contains only primes $\ll_C 1$ ?Source says proved (Lean)Formalized	proved (Lean)	In Lean	No Result decision
#912	Prove that there exists some $c>0$ such that $h(n) \sim c \left(\frac{n}{\log n}\right)^{1/2}$ as $n\to \infty$ .Source says openFormalized	open	In Lean	No Result decision
#1108	For each $k \geq 2$ , does the set $A = \left\{ \sum_{n\in S}n! : S\subset \mathbb{N}\text{ finite}\right\}$ of all finite sums of distinct factorials contain only finitely many $k$ -th powers?Source says openFormalized	open	In Lean	No Result decision