Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Terence Tao proves that
where is the least such that is a product of factors each at
most . The lower bound is Stirling's formula. The upper bound has two
steps. Tao's post proves the variant in the site's remark: is a product of
factors each at most . Tao does not use the greedy
decomposition but adapts the approximate-factorization method of
Alexeev and others 2025:
start from the integers in with no prime factor above
, each taken times, then add and remove factors to correct
the surplus or deficit of each prime, keeping the total waste
at . Pairing consecutive factors, as Stijn Cambie
observed and the site credits, then gives factors
each at most . The argument was posted in the site's discussion thread on
2026-01-03, written as the blueprint section "Erdos problem 392" of the Prime
Number Theorem And (PNT+) project on 2026-01-06, and formalized there in the
file Erdos392.lean, whose header says the proof is adapted from that post. The
formalization's contributors, as the file's history and Alexeev's source list
record them, are Tao, Pietro Monticone and Alex Kontorovich with the AI system
Aristotle; Tao announced its completion on 2026-02-23. The link pins the
revision that the formal-conjectures record names; the file at that revision
contains no sorry, axiom or native_decide, and it has not been built or
audited here, so it is a formalization link and gives no formalized evidence.
The file proves the two upper bounds, Solution_1 (factors at most ) and
Solution_2 (their pairing, factors at most ); the matching lower bound
from Stirling's formula is not in it. Nat Sothanaphan posted in the thread on
2026-02-26 a write-up dated 2026-02-25, generated by GPT-5.2 Thinking in a
near-autonomous process, that expands the same argument for factors at most
and pairs the factors for this problem.
The thread had started from the site's remark that the variant with factors at most has by a greedy decomposition, and from Stijn Cambie's observation that pairing consecutive factors of such a decomposition answers the question for . Participants doubted that the greedy argument proves the variant; the proof recorded here proves the variant by another method and reaches the asymptotic through Cambie's pairing, and Alexeev's source list names Cambie and Tao as the informal authors.
The site labels Problem 392 PROVED (LEAN); its page is linked above as a
discussion. Its commentary credits Cambie's pairing reduction and does not
name the author of the proof, so the label is not a curator's credit of this
result and no reviewed evidence is listed. The formal-conjectures file
FormalConjectures/ErdosProblems/392.lean tags the statement erdos_392 as
solved and names the PNT+ file above as its formal proof, while leaving its
own statement and Cambie's implication with sorry; that Lean has not been
built here, so no formalized evidence is listed either. No refereed write-up
is recorded. The claim is claimed, and the problem's
standing is claimed, proved, through this pending full claim.
Submission note. Posted to the site's forum by Terence Tao on 3 January 2026:
Here is a sketch of how the "modified approximate factorization method" can rigorously allow one to decompose as $n - \frac{n}{\log n} + o(\frac{n}{\log n})$ factors , as claimed by Erdos and Graham (but we will not use the greedy method). By the accounting identity and the Stirling approximation, it suffices to produce such that
- All are bounded above by .
- The total waste is .
- For every prime , the number of times divides matches the number of times divides .
The strategy of modified approximate factorization is to start with an approximate factorization that obeys 1 and 2 but not 3, and then add and remove factors to fix 3 without losing 1 or 2.
Let be large, let be small depending on , and suppose that is large depending on . The initial choice of the will be: all the integers between and that are not divisible by a prime larger than , with each integer repeated times. This obeys 1, and the total waste here is which will be good for us as we will eventually take to infinity. What about 3? The situation depends on the prime p:
3a (very large primes). If , then does not divide either $a_1 \dots a_t$ or . 3b (large primes). If , then divides times, but does not divide at all, thus one is short by copies of for each such . 3c (medium primes). If , then divides times and divides times, this one is either short or surplus by copies of . 3d (small primes). If $1/\varepsilon < p \leq \sqrt{n}$, then divides times and divides $a_1 \dots a_t$ times, so one is either short or surplus by copies of . 3e (tiny primes). If , then divides times and divides by times, so one is either surplus by $O(M \log n)$ copies or short by copies.
Now one fixes all the shortages and surpluses. For any medium, small, or tiny prime that is surplus, one simply deletes that prime from the relevant factor, generating in waste; because the primes are so small, the net waste in doing so adds up to which is acceptable. For the large, medium, or small primes that are short, one adds each such prime as a new factor, accepting an additional waste of ; the net cost here can be computed to be , which is also acceptable. The only remaining issue is with the short tiny primes , which are too numerous to add as individual factors; however, one can greedily bundle them into products of size between and , each generating of waste, plus at most one remainder term with of waste. Putting all this together, we can rebalance all the powers of while still keeping the net waste smaller than any given small multiple of , giving the claim.