Problem 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: erdosproblems.com/401

Number theory
Factorials

Wiki page

Status

SolvedProved

An accepted solution exists. The statement is true.

PROVED (LEAN). The site labels the problem PROVED (LEAN) (page last edited 12 January 2026) and credits a proof by Barreto and Leeham, working with ChatGPT, recorded on its claim page (Barreto Price, 2026); the Lean qualifier refers to the Aristotle-generated formalization of that proof in Boris Alexeev's repository, which this corpus has not built. A second route, the deduction from the Problem 729 construction that ChatGPT noticed and Nat Sothanaphan posted and checked, developed in the appendix of his write-up of Problem 728, is a pending claim on its own page. There is no refereed write-up. The standing in the frontmatter derives from the claim pages.

Problem 401

Status

Proof claims

Discussion