---

Claim. Ji Ho Bae, "Unbounded logarithmic limsup in Erdős Problem 684 via shifted carry scheduling", arXiv:2604.23784 (v3, 2026-09-03, 13 pages, CC BY 4.0), proves for the function $f(n)$ of Problem 684, the least $k$ for which the part of $\binom nk$ supported on primes at most $k$ exceeds $n^2$, that

$$\limsup_{n\to\infty}\frac{f(n)}{\log n}\cdot\frac{\log\log\log n}{\log\log n} \ge\frac12,$$

so that for every $\varepsilon>0$ there are infinitely many $n$ with $f(n)\ge(1/2-\varepsilon)\log n\,\log\log n/\log\log\log n$, and no bound $f(n)=O(\log n)$ holds. The claim's notes describe the method as a shifted-carry construction through a least common multiple, with product-cell coding, weighted Chinese-remainder tail counting and anchored-fiber selection, and the prime number theorem as the only analytic input. Versions 1 and 2 of the preprint (2026-04-26 and 2026-04-28) relied on a weighted extension of Timofeev's method that the author withdrew as unjustified; v3 is a complete rewrite and the only version claimed. The author's thread post of 2026-04-27 linked Zenodo record 19807164, which holds the withdrawn argument of versions 1 and 2 and not the claimed result, so it is not linked here. The result sits between the known bounds. [APSSV26], an unrefereed preprint carded at Alexeev, Putterman, Sawhney, Sellke and Valiant 2026 and recorded on the claim page Alexeev, Putterman, Sawhney, Sellke and Valiant 2026, reports an internal OpenAI model's elementary argument, edited by its five authors, that $f(n)\le(24/(\pi^2-6)+o(1))(\log n)^2$ for all large $n$ and $f(n)\ge(1/2+o(1))\log n$ along a sequence; Li's unrefereed preprint, carded at Li 2026, proves $f(n)=(2/(1-\gamma)+o(1))\log n$ for almost all $n$. So Bae's bound shows that the worst case grows faster than the typical case and leaves the extremal order between $\log n\,\log\log n/\log\log\log n$ and $(\log n)^2$.

Submission note. Posted to erdosproblems.com as a proof claim by Ji Ho Bae (account jidodae) on 4 September 2026:

I claim that the new lower bound, combined with the cited upper bound, fully answers "Give bounds for $f(n)$," the modern form of Erdős's question "we do not know how fast." Upper bound (Alexeev et al., arXiv:2603.29961): for all large $n$, $f(n)\le\left(\frac{24}{\pi^2-6}+o(1)\right)(\log n)^2$. Their earlier lower bound was $f(n)\ge\left(\tfrac12-o(1)\right)\log n$ infinitely often. New lower bound (this work, arXiv:2604.23784v3): unconditionally, $\limsup_{n\to\infty}\frac{f(n)}{\log n}\cdot\frac{\log\log\log n}{\log\log n}\ge\tfrac12$; equivalently, $f(n)\ge\left(\tfrac12-o(1)\right)\log n,\frac{\log\log n}{\log\log\log n}$ infinitely often. Thus $f(n)>C\log n$ infinitely often for every $C>0$, but $f(n)=O((\log n)^2)$; in particular, $f(n)=O(\log n)$ is impossible. The exact extremal order is a separate, stronger question and remains open. Notes: Erdős source: P. Erdős, "Some unconventional problems in number theory," Acta Math. Acad. Sci. Hungar. 33 (1979), 71–80, at pp. 76–77, https://doi.org/10.1007/BF01903382; his $A(n)$ is $f(n)$ here. Method: LCM shifted-carry proof with product-cell coding, weighted CRT tail counting, and anchored-fibre selection; PNT is the sole analytic input. Only arXiv:2604.23784v3 is claimed (the weighted extension of Timofeev's method in v1–2 was unjustified and is withdrawn; v3 is an independent complete rewrite). Lean 4 + Mathlib; PNT via MediumPNT in PrimeNumberTheoremAnd (Kontorovich, Tao et al.); no unproved hypotheses or sorry; axioms only propext, Classical.choice, Quot.sound. AI-assisted under my direction and review. Palomar: PALOMAR-2026-09-03-000006 v1, https://palomar-registry.org/entry?id=PALOMAR-2026-09-03-000006&version=1 Source: https://github.com/jidodat/erdos684-lean (tag v3-arxiv)

The Palomar registry's description of entry PALOMAR-2026-09-03-000006:

A Lean 4 formalization, against Mathlib, of the main theorem of J. H. Bae, "Unbounded logarithmic limsup in Erdős Problem 684 via shifted carry scheduling" (arXiv:2604.23784, v3). For 0 ≤ k ≤ n write C(n,k) = u·v with u supported on the primes ≤ k and v on the primes in (k,n], and let f(n) be the least k with u > n²; Erdős asked for bounds on f(n) (Problem 684 in Bloom's database). The compared theorems state that for every ε > 0 there are infinitely many n with f(n) > (1/2 − ε)·log n·log log n / log log log n, equivalently limsup f(n)·log log log n /(log n·log log n) ≥ 1/2 (stated in the extended nonnegative reals), and in particular that f(n)/log n is unbounded, so no estimate f(n) = O(log n) holds. This strengthens the subsequential lower bound (1/2 − o(1)) log n of Alexeev–Putterman–Sawhney–Sellke–Valiant by a factor of order log log n / log log log n; the general upper bound (log n)² remains the best known and the exact order of f(n) is open. Two further compared statements fix the meaning of the definitions: u(n,k) times the part of C(n,k) supported on primes exceeding k equals C(n,k), and K < f(n) holds exactly when u(n,k) ≤ n² for all 1 ≤ k ≤ min(K,n). The proof follows the paper section by section (Kummer carries, a product-cell code, a CRT count with exponential weighting, an anchored-fibre selection lemma, and a four-range carry budget). The prime number theorem is the single analytic input: the library proves the theorem under the explicit hypothesis θ(x) = x + O(x/log² x) and then discharges that hypothesis from the bound ψ(x) = x + O(x·exp(−c(log x)^{1/10})) of the PrimeNumberTheoremAnd project (Kontorovich, Tao et al.), so the compared theorems carry no hypotheses and depend only on propext, Classical.choice and Quot.sound.

Covers. The lower bound along a sequence of $n$ stated above, and with it the failure of $f(n)=O(\log n)$. It does not determine how fast $f(n)$ grows: the claimant says that the true order of $f(n)$ is a further, harder question and leaves it open, and the site's curator asks whether $f(n)\gg(\log n)^2$ holds infinitely often.

Depends on. No page of this wiki.

Formalization. The repository jidodat/erdos684-lean, pinned at its tag v3-arxiv, defines $u(n,k)=\prod_{p\le k}p^{\nu_p\binom nk}$ and $f(n)=\min\{1\le k\le n:u(n,k)>n^2\}$ with $f(n)=\infty$ when no $k$ qualifies, and proves main_theorem_unconditional: for every $\varepsilon>0$, for infinitely many $n$, every $k$ with $k\le(1/2-\varepsilon)\log n\,\log\log n/\log\log\log n$ satisfies $k<f(n)$. It builds with Lean 4.32 and Mathlib; the prime number theorem enters from the PrimeNumberTheoremAnd project in the form $|\theta(x)-x|\le Cx/(\log x)^2$, and the README reports only the axioms propext, Classical.choice and Quot.sound and no sorry. The Palomar registry entry PALOMAR-2026-09-03-000006 (version 1, 2026-09-03) records a replay of the proof in the Lean kernel against a challenge statement; the registry says that it certifies neither novelty nor the match between the formal and informal statements and is not peer review. This corpus has not built the development, so these are formalization and record links and give no formalized evidence.

Authorship and tools. The claim's notes say the work was AI-assisted under the author's direction and review; they name no system.

Standing. Submitted on the problem's proof-claims tab as a full claim on 2026-09-04, asserting that together with the upper bound of [APSSV26] it answers the request for bounds on $f(n)$. The site's curator, Thomas Bloom, changed it to a partial claim the same day, since the two bounds leave the growth of $f(n)$ uncertain, and a commenter observed that the result rules out an asymptotic $f(n)\sim c\log n$ of the kind that the density-one results suggest for most $n$. The preprint is not refereed and no outside reviewer has recorded accepting it, so the claim is claimed. The site labels the problem OPEN (page last edited 1 April 2026) and its remarks do not mention the preprint.