Unbounded logarithmic limsup in Erdős Problem 684 via shifted carry scheduling
Ji Ho Bae
math.NT
Apr 26, 2026 · v3
math.CO
TL;DR
The main theorem on Erdős Problem 684 is fully formalized and machine-checked in Lean 4 with Mathlib, following the paper section by section.
Abstract
For $1\leq k\leq n$, let $u(n,k)=\prod_{p\leq k}p^{ν_p\binom nk}$ and $f(n)=\min\{1\leq k\leq n:u(n,k)>n^2\}$. The minimum is interpreted as $+\infty$ if the set is empty. Here $ν_p(m)$ denotes the exponent of the prime $p$ in $m$. Erdős Problem 684 asks for bounds on $f(n)$. We prove $\limsup_{n\to\infty} \frac{f(n)}{\log n}\frac{\log\log\log n}{\log\log n}\geq\frac12$. In particular, $\limsup_{n\to\infty}f(n)/\log n=\infty$, so no uniform estimate $f(n)=O(\log n)$ is possible. The proof constructs integers $n=tL_M-h-1$, where $L_M=\operatorname{lcm}(1,\ldots,M)$. Product-cell coding yields simultaneous two-sided approximations to $tL_M$ modulo every prime in $(M,K]$. Writing $n+1=tL_M-h$, the shift by $h$ folds both signs into the same one-sided carry region. The carries at levels at most $M$ are bounded by $\log\binom{h+k}{h}$. For the prime powers above $K$, a truncated CRT witness has modulus below the search range; exponential weighting then gives an exponentially small exceptional set. An elementary anchored-fibre lemma selects a multiplier satisfying both requirements. Together, these ingredients prove the stated bound unconditionally. The theorem has been formally verified in Lean 4 with Mathlib.
Problem
Erdős Problem 684 asks for bounds on f(n), the least k for which the part of the binomial coefficient C(n,k) supported on primes at most k exceeds n^2. The best previously known worst-case lower bound was f(n) ≥ (1/2+o(1)) log n along a subsequence.
Approach
The proof constructs n = tL_M − h − 1 with L_M = lcm(1,…,M). Product-cell coding gives simultaneous approximations to tL_M modulo primes in (M,K], and the shift h folds both signs into a one-sided carry region. Carries at prime-power levels up to M are bounded by log C(h+k,h). High prime powers are controlled by a CRT and exponential-weighting tail estimate, and an anchored-fibre pigeonhole lemma selects a suitable multiplier. The whole argument is formalized in Lean 4 using only Mathlib, and #print axioms reports only the three standard axioms.
Results
The paper proves limsup f(n)/log n · logloglog n/loglog n ≥ 1/2. Hence f(n)/log n is unbounded and f(n) = O(log n) cannot hold. The theorem is machine-checked in Lean 4.