A Greatest Common Divisor Criterion of Certain Binomial Coefficients
2026-06-22 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors proved a math rule about the greatest common divisor (gcd) of certain binomial coefficients, which was previously a conjecture listed by Ralf Stephan. Specifically, for numbers defined by k, they studied the gcd of combinations like (qk choose k) and found a condition involving prime-power factors of k+1. Their proof was fully written and checked using a computer program called Lean. They used an AI system they developed, called MechMath Agent Team, to create both the traditional proof and the computer version.
greatest common divisorbinomial coefficientprime powerOEISLean theorem proverformal proofconjecturecombinatoricsAI-assisted proof
Authors
Dakai Guo, Ruichen Qiu, Yichuan Cao, Ruyong Feng, Xiao-Shan Gao
Abstract
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.