Problem 459

../

claims/: The 1 claim page of Problem 459, one per claimant's result; the problem's standing derives from them.

---

Statement. Let $f(u)$ be the largest $v$ such that no $m\in (u,v)$ is composed entirely of primes dividing $uv$. Estimate $f(u)$.

Status. SOLVED (LEAN), on the site's label: the curator credits Stijn Cambie's observations, that $f$ attains each of its trivial bounds $u+2$ and $u^2$ infinitely often while $f(n)=(1+o(1))n$ for almost all $n$, as settling the natural readings of an estimate question whose intended precision the site calls unclear, and records Lean proofs of these statements outside this corpus; all of this is on the claim page. The Lean proofs are not built here.

Source. erdosproblems.com/459, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #459, https://www.erdosproblems.com/459.

Formalization. Statement in formal-conjectures, pinned at its commit of 18 September 2026, whose formal_proof attribute points to the Lean file in van Doorn's repository linked from the claim page, beside Alexeev's earlier file it extends; neither is built or audited here.

Progress

Not yet compiled.

Known Results

Not yet compiled.