We resolve Erdős Problem 731 under the explicit dyadic-regularity formalization of "reasonable." Let A(n) be the least positive integer not dividing \binom2nn. On dyadic intervals X≤ n<2X, put L=log(2X) and FX=√(2)(log 2)1/4L1/4exp√((log 2)L). Uniformly for 1≤ z≤ Z(X)=o(L1/4), we prove ℙX(A(n)≤ FXexp(-z))\asymp exp(-2z) and ℙX(A(n)>FXexp(z))≪ exp(-2z). Consequently log A(n)=√((log 2)log n)+(1)/(4)loglog n+Odens(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)→ 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.