{"id":"arxiv/2606.22997","url":"https://arxiv.org/abs/2606.22997","tags":["math.NT","cs.LO"],"score":0,"title":"A Greatest Common Divisor Criterion of Certain Binomial Coefficients","domain":"math.NT","source":"arxiv","authors":["Dakai Guo","Ruichen Qiu","Yichuan Cao","Ruyong Feng","Xiao-Shan Gao"],"reviews":0,"subject":"math.NT","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-06-22","reactions":{}}