A Greatest Common Divisor Criterion of Certain Binomial Coefficients

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.