---

Claim. The answer to Problem 730 is yes, with consecutive pairs: there are infinitely many $n$ such that $\binom{2n}{n}$ and $\binom{2n+2}{n+1}$ have the same set of prime divisors, and for all sufficiently large $x$ the number of such $n\le x$ is at least a constant times $x^{1/2}$. The site's commentary states the result in this form; the formalization below proves the set of such $n$ infinite, by way of a positive lower density for a quadratic family. Liam Price (the forum user Leeham) posted the result to the site's discussion thread on 2026-06-24, which dates this page, and submitted it as the problem's proof claim on 2026-07-15 with a link to the proof document; the argument was produced by the AI system GPT Pro, which the claimant names while noting that the model running under that name in the chat application that week was believed to be GPT-5.6 Pro.

Submission note. Posted to erdosproblems.com as a proof claim by Liam Price (account Leeham) on 15 July 2026, giving "GPT Pro" as the AI used, which the site marks as accepted as correct:

GPT Pro, in fact, can show the stronger result that there are infinitely many such pairs which are consecutive. Notes: During the week this proof was given, many people claimed GPT-5.6 Pro was being tested in the chatgpt app and I tended to agree with them, however as this isn't official I gave just "GPT-Pro" as the model.

Posted to the site's forum by Liam Price on 24 June 2026:

GPT Pro, in fact, can show the stronger result that there are infinitely many such pairs which are consecutive. Here is the general gist of its argument:

The proof begins by converting equality of prime supports into a problem about base-$p$ digits. Kummer's theorem then shows that a prime can disappear from $\binom{2n}{n}$ or appear in $\binom{2n+2}{n+1}$ only when a certain quotient associated with $n+1$ or $2n+1$ has all its base-$p$ digits at most $(p-1)/2$. We then construct an explicit quadratic family for which $n+1=PQ$ and $2n+1=3RS$, where $P,Q,R,S$ are pairwise separated linear forms, so that every possible obstruction is attached to exactly one of four branches. On each branch, after fixing a prime divisor and parametrising the corresponding congruence class, the relevant quotient becomes a quadratic polynomial whose linear coefficient is a $p$-adic unit. This gives strong permutation properties modulo powers of $p$. Fourier analysis and bounds for incomplete quadratic sums then show that, on blocks of length $p^r$, the proportion of values whose first $2r$ base-$p$ digits are all restricted is essentially $4^{-r}$. The proof then concludes with some case checking on some obstruction prime range sizes.

The argument. Since $\binom{2n+2}{n+1}=\binom{2n}{n}\cdot2(2n+1)/(n+1)$, a prime can leave the support only by dividing $n+1$ and can enter it only by dividing $2n+1$, and Kummer's theorem, by which an odd prime $p$ divides $\binom{2n}{n}$ exactly when some base-$p$ digit of $n$ is at least $(p+1)/2$, turns each event into a digit condition: if $p^j$ exactly divides $n+1$, the prime leaves only when every base-$p$ digit of $(n+1)/p^j$ is at most $(p-1)/2$, and if $p^j$ exactly divides $2n+1$, so that the low $j$ digits of $n$ are all $(p-1)/2$, it enters only when every base-$p$ digit of $\lfloor n/p^j\rfloor=((2n+1)/p^j-1)/2$ is at most $(p-1)/2$. Price's summary speaks of a quotient associated with $n+1$ or $2n+1$. The proof takes an explicit quadratic family of $n$ with $n+1=PQ$ and $2n+1=3RS$ for pairwise separated linear forms $P,Q,R,S$, so that every possible obstruction belongs to one of four branches; on each branch, after fixing a prime divisor and parametrizing its residue class, the quotient is a quadratic polynomial whose linear coefficient is a $p$-adic unit, which gives permutation properties modulo powers of $p$. Fourier analysis with bounds for incomplete quadratic sums shows that on blocks of length $p^r$ the proportion of parameters whose first $2r$ base-$p$ digits are all restricted is about $4^{-r}$, and a count over the sizes of the obstruction primes finishes the proof. A forum user, Tomodovodoo, posted on 2026-06-25 a closing derivation of the algebraic skeleton from the model's reasoning traces, which the formalization credits.

Formalization. Will Blair's repository of Lean proofs, linked above at the commit that the Palomar registry verified (2026-08-22), declares itself a formalization of this argument in its provenance file formalization.yaml, which names Blair as its author, Price's thread post and Tomodovodoo's route mapping as its sources, and Codex and Claude Code agent sessions as its automation; that file says the development was built from the public summary and the route mapping, with the analytic sections reconstructed by the formalizer, and that it proves the stronger statement that infinitely many consecutive pairs exist by giving the quadratic family a positive lower density (Kummer's theorem, a fixed-depth Fourier estimate, a Mertens-type input, and the prime number theorem in arithmetic progressions through an external library). The registry entry, linked as a record, checked the statement S.Infinite for the pair set of the formal-conjectures file against a Challenge importing Mathlib alone, with the axioms propext, Classical.choice and Quot.sound; the formal-conjectures statement file names that proof as the problem's formal proof, and a copy of the development in Boris Alexeev's repository of formalized Erdős problems, linked at its pinned commit, states both the consecutive-pair theorem and the pair-set theorem under a header naming Price, Tomodovodoo, Blair and GPT Pro as the informal authors and Blair, Codex and Claude Code as the formal authors. The provenance file's review entry is self-assessed and says that no independent human review of the mathematics had been performed. This corpus has not built or audited any of these developments, so the page lists no formalized evidence.

Depends on. No page of this wiki.

Acceptance. Thomas Bloom, the site's curator, marks the problem solved, credits GPT Pro prompted by Price on the problem page (last edited 1 September 2026), and the proof-claim entry carries the site's statement that the proof has been accepted as correct; the page lists this as reviewed. Nothing is refereed, and the proof document is an Overleaf manuscript rather than a preprint server posting. The community database's row for the problem records the status solved (last update 2025-08-31) and the formal status unformalized, so the site's own page and its proof-claim entry are the record of acceptance.