A Resolution of Erdős Problem 731 under Dyadic Regularity

Abstract

We resolve Erdős Problem 731 under the explicit dyadic-regularity formalization of "reasonable." Let $A(n)$ be the least positive integer not dividing $\left(\genfrac{}{}{0ex}{}{2n}{n}\right)$. On dyadic intervals $X\le n<2X$, put $L=\log (2X)$ and $F_X=\sqrt{2}(\log 2{)}^{1/4}{L}^{1/4}\exp \sqrt{(\log 2)L}$. Uniformly for $1\le z\le Z(X)=o(L^{1/4})$, we prove ${\mathbb{P}}_X(A(n)\le F_X\exp (-z))\asymp \exp (-2z)$ and ${\mathbb{P}}_X(A(n)>F_X\exp (z))\ll \exp (-2z)$. Consequently $\log A(n)=\sqrt{(\log 2)\log n}+\frac{1}{4}\log \log n+O_{\mathrm{dens}}(1)$. We also prove dyadic nonconcentration: no scalar center on a large dyadic block, and hence no dyadically regular deterministic scale $f$, can satisfy $A(n)/f(n)\to 1$ in natural density. The proof retains the exact least-common-multiple divisibility condition and replaces heuristic cross-base independence by a moving-base restricted-digit variance theorem. The resolution proved here has been formally verified in Lean.

v2: The resolution proved in this paper has been formally verified in lean. 24 pages