# A Greatest Common Divisor Criterion of Certain Binomial Coefficients

arXiv: https://arxiv.org/abs/2606.22997 · HTML: https://mlsanity.com/paper/2606.22997/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 22 Jun 2026.

## Built on by (most cited first, 1 of 1)

- [MechMath Agent Team: LLM Driven Agents for Mathematical Research](https://mlsanity.com/paper/2607.04394/) (2026)

## Abstract (arXiv)

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≥ 2, put [ D(k)=gcd2≤ q≤ k+1binomqkk, qquad n=k+1. ] If P is the largest prime-power component pa exactly dividing n, then the criterion asserts [ D(k)=1 quadLongleftrightarrowquad fracnP>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.