← All papers
A Greatest Common Divisor Criterion of Certain Binomial Coefficients
math.NT
Jun 22, 2026 · v1
cs.LO
TL;DR
Formalizes in Lean the proof of the OEIS A080170 binomial gcd criterion, accepted into the Formal Conjectures project.
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.
Problem
Prove the binomial gcd criterion recorded as OEIS A080170, also listed as conjecture (17) in Ralf Stephan's OEIS conjectures.
Approach
For D(k)=gcd of binom(qk,k) over 2<=q<=k+1 and n=k+1, the criterion asserts D(k)=1 iff n/P>P, where P is the largest prime-power dividing n. Both the natural-language proof and the Lean formalization were generated by the authors' MechMath Agent Team.
Results
The criterion is proven and the Lean artifact is accepted as part of the Formal Conjectures project.