---

Claim. Read $f(u)$, as the site's remark and every formalization do, as the least $v>u$ all of whose prime factors divide $u$; the site states this is equivalent to the definition of Problem 459. For $u\geq 2$ the integer $u+1$ has a prime factor not dividing $u$, and $u^2$ has none, so

$$u+2\leq f(u)\leq u^2.$$

Stijn Cambie's observations, credited by the site, are these. When $u=p$ is prime, $f(p)=p^2$, since the only candidates are the powers of $p$. When $u$ is even, every power of $2$ is a candidate, so $f(u)\leq 2^k$ for the least power $2^k>u$; for $u=2^k-2$ with $k\geq 2$ that power is $u+2$, so $f(u)=u+2$. Both bounds are therefore attained infinitely often and $f$ has no regular order of growth. For the typical $n$, however, $f(n)=(1+o(1))n$: for every $\varepsilon,\delta>0$ there is an $x_0$ such that, for every $x\geq x_0$, at least $(1-\delta)x$ of the integers $n\leq x$ satisfy $f(n)<(1+\varepsilon)n$. Cambie's argument, posted in the site's discussion on 6 February 2026, fixes $M$ so that all but a $\delta/2$ proportion of the integers are divisible by two distinct primes $p,q<M$; for each such pair, because $\log p/\log q$ is irrational, the integers of the form $p^aq^b$ have consecutive ratios tending to $1$, so for every large $n$ divisible by $pq$ one of them lies in $(n,(1+\varepsilon)n]$ and has all its prime factors dividing $n$.

The problem asks only to estimate $f(u)$, and the site's remark says that the estimates Erdős and Graham had in mind are not clear; the curator marks the problem solved because these observations answer the natural readings of the question. The exact order of the exceptional set, and any finer statistic of $f$, are outside this claim.

Acceptance. The site's curator, Thomas F. Bloom, marks Problem 459 solved and credits Cambie's observations, the reviewed evidence; no journal publication is recorded. The page is dated by the earliest record of the remark crediting Cambie: the Wayback Machine snapshot of the site's page taken on 13 September 2025, linked above as the record, shows the label SOLVED, the remark and the acknowledgment of Cambie, while the snapshot of 15 September 2024 shows the problem open without the remark; the community database (teorth/erdosproblems) lists the problem as solved, as of its last update of the entry on 31 August 2025. The proof of the almost-all estimate was posted in the site's discussion on 6 February 2026, and the observations may be older than any of these dates.

Formalization. Three Lean files, linked above, formalize these statements for the function $f$ defined as above, the earliest only in part; all three are formalizations of the results the site credits to Cambie, so they are links on this page and not claims of their own. Boris Alexeev's Erdos459b.lean in their lean-proofs repository, pinned at the commit of 6 February 2026 in the link, carries no header, author line or attribution; Alexeev's post in the site's discussion of 6 February 2026 presents it as a formalization of some of the results in the problem's description, which are those credited to Cambie. The file proves the two bounds, $f(p)=p^2$, the bound $2^k$ for even $u$, $f(2^k-2)=2^k$, and that each bound is attained infinitely often; the post says that it is not complete, lacking the almost-all estimate. The same repository's later src/latest/ErdosProblems/Erdos459.lean, pinned in the link at a commit of 24 August 2026, carries a header that names Cambie as the informal author and Aristotle, Alexeev and van Doorn as the formal authors. It proves every statement of Alexeev's earlier file and, as its theorem erdos_459, the almost-all estimate. Wouter van Doorn's ErdosProblem459.lean in their Lean-files repository, pinned at the commit of 11 March 2026, is Alexeev's file extended with the almost-all estimate, formalized by Aristotle (Harmonic): its main_theorem states, for $\varepsilon,\delta>0$, an $x_0$ beyond which at least $(1-\delta)x$ of the $n\leq x$ have $f(n)<(1+\varepsilon)n$, under leanprover/lean4:v4.24.0; its 724 lines contain no sorry, axiom or native_decide token. The formal_proof attribute of the statement in google-deepmind/formal-conjectures names van Doorn's file for the two bounds and for $f(p)=p^2$. This corpus has built none of these files, so no formalized evidence is listed, and the formal-conjectures statement file is not a formalization link.

Depends on. Nothing beyond the postings linked above.