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.
From: Dakai Guo [view email]
[v1]
Mon, 22 Jun 2026 08:14:01 UTC (21 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。