← All papers
First page of Unbounded logarithmic limsup in Erdős Problem 684 via shifted carry scheduling

Unbounded logarithmic limsup in Erdős Problem 684 via shifted carry scheduling

Ji Ho Bae

math.NT Apr 26, 2026 · v3 math.CO
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.
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.

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.

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.

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.