Does there exist a function f:N→R with f(r)→∞ as r→∞ such that, for every r∈N with r≥1, there are infinitely many n∈N for which there exist a_1,a_2∈N with a_1>0, a_2>0, a_1+a_2>n+f(r)log n, and a_1!a_2!| n!(∏_i=0^r-1p_i)^n, where p_i denotes the ith prime?

Erdős Problem #401 — Large Factorial Divisors

About 46 years old · traced to 1980

Does there exist a function $f:\mathbb{N}\to\mathbb{R}$ with $f(r)\to\infty$ as $r\to\infty$ such that, for every $r\in\mathbb{N}$ with $r\geq1$ , there are infinitely many $n\in\mathbb{N}$ for which there exist $a_1,a_2\in\mathbb{N}$ with $a_1>0$ , $a_2>0$ ,

a_1+a_2>n+f(r)\log n,

and

a_1!a_2!\mid n!\left(\prod_{i=0}^{r-1}p_i\right)^n,

where $p_i$ denotes the $i$ th prime?

References

Primary source

The Formal Conjectures Authors, Formal Conjectures (2025); independently edited from the pinned source file.

Additional references

Pinned Formal Conjectures source, Apache-2.0.

factorials number-theory

InErdős Problems

Posted 2 months ago · edited 3 weeks ago

Progress summary

Refreshed 1 month ago

Claimed solved

A formal proof now confirms that the requested function exists, so the problem is solved, although a stronger version requiring the condition for every sufficiently large number is false.

Problem $401$ asks whether there is an unbounded function $f(r)$ for which infinitely many $n$ satisfy the stated factorial divisibility and size conditions.

January 2026 formal resolution

A formal result proves that, for infinitely many triples $(a,b,n)$ , one has $a!b!\mid n!(a+b-n)!$ with $a+b-n$ comparable to $\log n$ ; the paper explains that these examples imply the required unbounded $f(r)$ . The proof uses $p$ -adic inequalities, Kummer’s theorem, and carry-counting, and was formalized in Lean. The stronger interpretation requiring the assertion for all sufficiently large $n$ is false.

Current status (as of April 2026): Problem $401$ is resolved by a formal Lean proof; only the stronger all- $n$ variant remains false rather than open.

AristotleHarmonicsolved2026-01-01evidence

Sources

No solutions have been posted yet.