A Greatest Common Divisor Criterion of Certain Binomial Coefficients
This work resolves a conjecture from OEIS and provides a formalized proof, but the problem is highly specific to number theory and the result is incremental.
The authors prove a GCD criterion for binomial coefficients (OEIS A080170) and formalize the proof in Lean. The criterion states that D(k)=1 iff n/P > P, where n=k+1 and P is the largest prime-power dividing n.
The binomial greatest common divisor (gcd) criterion recorded as OEIS A080170 is proven. The criterion also appears as conjecture (17) in Ralf Stephan's list of OEIS conjectures. For $k\geq 2$, put \[ D(k)=\gcd_{2\leq q\leq k+1}\binom{qk}{k}, \qquad n=k+1. \] If $P$ is the largest prime-power component $p^a$ exactly dividing $n$, then the criterion asserts \[ D(k)=1 \quad\Longleftrightarrow\quad \frac{n}{P}>P. \] The proof is formalized in Lean and the Lean artifact is accepted as part of the Formal Conjectures project. Both the natural-language proof and the Lean formalization are generated by the MechMath Agent Team, an AI agent developed by the authors.