---

Claim. Let $A(n)$ be the least $m\ge1$ with $m\nmid\binom{2n}n$, the quantity Problem 731 asks to describe by a reasonable $f$ with $A(n)\sim f(n)$ for almost all $n$. The preprint Eric Li, A Resolution of Erdős Problem 731 under Dyadic Regularity, arXiv:2606.29062 (submitted 27 June 2026, revised 26 July 2026; carded as Li 2026), proves three things. With $L=\log(2X)$ and

$$\mathcal F_X=\sqrt2\,(\log2)^{1/4}L^{1/4}\exp\sqrt{(\log2)L},$$

Theorem 1.3 gives, on every sufficiently large dyadic block $X\le n<2X$ and uniformly for $1\le z\le Z(X)=o(L^{1/4})$, the tail bounds $\mathbb P_X(A(n)\le\mathcal F_Xe^{-z})\asymp e^{-2z}$ and $\mathbb P_X(A(n)>\mathcal F_Xe^{z})\ll e^{-2z}$. Corollary 1.7 turns this into the global statement that $\log A(n)-\sqrt{(\log2)\log n}-\tfrac14\log\log n$ exceeds a bound $C$ in absolute value only on a set whose upper density tends to $0$ as $C\to\infty$, so $F(n)=\sqrt2(\log2)^{1/4}(\log n)^{1/4}\exp\sqrt{(\log2)\log n}$ is the density-tight scale, sharpening the $\exp((\log n)^{1/2+o(1)})$ that Erdős, Graham, Ruzsa and Straus stated. Theorem 1.10 shows that no dyadically regular $f$, meaning a positive $f$ whose $\log f$ varies over the dyadic block $X\le n<2X$ by an amount tending to $0$ as $X\to\infty$, satisfies $A(n)/f(n)\to1$ in natural density, because $A(n)$ keeps a fixed multiplicative spread on a positive proportion of every large block (Theorem 1.4). The method keeps the exact least-common-multiple condition, reduces through Kummer's theorem to carry-free prime events, and replaces a heuristic independence across bases by a moving-base restricted-digit variance estimate built on an additive large sieve.

Submission note. Posted to erdosproblems.com as a proof claim by Eric Li (account EricLi) on 17 July 2026, giving "GPT-5.5 Pro" as the AI used:

We resolve Erdős Problem 731 under the explicit dyadic-regularity formalization of "reasonable." For

$$A(n)=\min\{m\ge1:m\nmid \binom{2n}{n}\}, >$$

and on $X\le n<2X$, with $L=\log(2X)$ and

$$\mathcal > F_X=\sqrt2\,(\log2)^{1/4}L^{1/4}\exp\sqrt{(\log2)L},$$

we prove, uniformly for

$1\le z\le Z(X)=o(L^{1/4})$,

$$\mathbb{P}_X(A(n)\le \mathcal > F_X\,\mathrm{e}^{-z})\asymp \mathrm{e}^{-2z},\qquad \mathbb{P}_X(A(n)>\mathcal > F_X\,\mathrm{e}^{z})\ll \mathrm{e}^{-2z}.$$

Thus $\log A(n)-\sqrt{(\log2)\log

n}-\frac14\log\log n$ is tight in natural density, while no dyadically regular deterministic scale satisfies the requested asymptotic equivalence. The proof keeps the exact least-common-multiple condition and replaces heuristic cross-base independence by a moving-base restricted-digit variance estimate. Notes: The answer has two parts. First, $F$ is the best possible deterministic scale for logarithmic density-tightness. Second, the original request $A(n) ∼ f(n)$ cannot be met by any dyadically regular $f$, because $A(n)$ retains fixed-size multiplicative nonconcentration on every sufficiently large dyadic block. Additionally, what dyadic regularity excludes is also exactly what the word “reasonable” is meant to exclude.

Formulation. The claim is full only on the author's reading of "reasonable" as dyadically regular, under which the requested equivalence cannot be met and $F$ is the best deterministic scale in the density-tight logarithmic sense. The problem's source does not define "reasonable", and the theorems say nothing about functions outside the dyadically regular class. The paper is unverified and disputed: the comments on the problem's discussion thread of 30 June and 1 July 2026 question the volume of the author's simultaneous claims, ask whether any verification was carried out, and dispute the credit given to the AI assistance, while the reading of "reasonable" itself is not contested there; the claim page keeps the author's scope and leaves the reading to be judged.

Formal verification in the claimant's repository. The repository linked above at a pinned commit holds a Lean 4 development which its README says was produced by Aristotle, Harmonic's automated theorem prover. Its headline theorems no_dyadically_regular_equivalent_unconditional and global_density_tight_unconditional carry no hypotheses and are built, with a prime number theorem by Newman's Tauberian argument and a Gallagher-type large sieve, on Mathlib alone; the author's verification file reports the axioms propext, Classical.choice and Quot.sound for them. The development proves the two headline theorems through the fixed-$z$ form of Theorem 1.3 (mesoscopicTailBounds_per_z), the only form the two proofs use, and not the statement uniform in $z$ that the paper gives. This corpus has not built or audited the development, so no formalized evidence is listed.

Depends on. No page of this wiki.

Claimant and systems. Eric Li posted the result as the first version of the arXiv preprint on 2026-06-27, which dates this page, and submitted it to the site's proof-claims tab on 2026-07-17 as a full resolution; the tab names GPT-5.5 Pro, the paper discloses extensive assistance from language models, and the Lean development was produced by Aristotle (Harmonic), as the author's comment of 1 July 2026 on the discussion thread and the repository's README state.

Standing. Pending. The site's label is open and its page, last edited 19 October 2025, predates the claim; the proof-claims entry carries no comments, the preprint is not refereed, and this corpus has checked neither the paper nor the Lean development.