Problem 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$ . Is it true that

A(n)=\frac{n}{2}-\frac{n}{2\log n}+o\left(\frac{n}{\log n}\right)?

Source: erdosproblems.com/392

Number theory
Factorials

Wiki page

Status

ClaimedProved

A full solution has been claimed but not yet accepted. The statement is true.

The site labels the problem PROVED (LEAN). The standing derived from the claim pages is claimed, proved, through the pending full claim Tao 2026: the site's commentary credits only Cambie's pairing reduction and does not name the proof's author, and the Lean formalization in the PNT+ project is third-party work not built here, so the claim lists no acceptance evidence.

Problem 392

Status

Proof claims

Discussion