🔢 mathematics

A Greatest Common Divisor Criterion of Certain Binomial Coefficients

This paper presents a formal proof, generated by the AI-driven MechMath Agent Team and verified in Lean, of the OEIS A080170 criterion which establishes that the greatest common divisor of specific binomial coefficients equals one if and only if the quotient of $n=k+1$ by its largest prime-power factor exceeds that factor.

Original authors: Dakai Guo, Ruichen Qiu, Yichuan Cao, Ruyong Feng, Xiao-Shan Gao

Published 2026-06-23

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Dakai Guo, Ruichen Qiu, Yichuan Cao, Ruyong Feng, Xiao-Shan Gao

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

The Big Picture: A Digital Detective Story

Imagine you have a giant, infinite library of number patterns called the OEIS (The On-Line Encyclopedia of Integer Sequences). It's like a massive catalog where mathematicians write down interesting lists of numbers they've found.

For a long time, one specific entry in this library, labeled A080170, was a mystery. It listed numbers that shared a very special, boring property: they had no common divisors other than 1. (In math terms, their "Greatest Common Divisor" is 1).

The library had a guess (a conjecture) about why these numbers behaved this way. It suggested that the answer depended on the "building blocks" of the number right next to it. But nobody had proven the guess was true. It was just a hunch.

This paper is the story of how a team of human mathematicians and an AI agent called MechMath solved this mystery, proved the guess was correct, and even built a "robot proof" that a computer could check to ensure no mistakes were made.

The Puzzle: The "Binomial" Lock

To understand the puzzle, imagine you have a special lock made of Binomial Coefficients. You might know these as the numbers in Pascal's Triangle (the triangle of numbers used to calculate probabilities or expand algebraic expressions).

The puzzle asks: If you take a specific number, let's call it $k$ , and look at a specific row of numbers generated by multiplying $k$ by different numbers ( $2k, 3k, 4k...$ ), do all those resulting numbers share a common factor?

The Question: Is the "Greatest Common Divisor" (GCD) of all these numbers equal to 1? (Meaning, do they have no shared factors?)
The Guess: The guess said, "Yes, the GCD is 1 if and only if the number next to $k$ (which is $k+1$ ) has a specific shape."

The Shape of the Number: The "Tallest Tower" Analogy

To understand the condition, imagine the number $n = k + 1$ is a castle built out of prime number bricks (like 2, 3, 5, 7, etc.).

Every number can be broken down into these bricks. For example, if $n = 12$ , it's made of $2 \times 2 \times 3$ .

The "bricks" come in stacks. You have a stack of 2s (height 2) and a stack of 3s (height 1).
The paper focuses on the tallest stack of identical bricks. In the case of 12, the tallest stack is the two 2s.

The Rule (The Criterion):
The paper proves that the GCD is 1 (the lock is "open") if and only if the rest of the castle (the part not in the tallest stack) is bigger than the tallest stack itself.

If the rest of the castle is huge: The lock opens (GCD = 1).
If the tallest stack is as big as or bigger than the rest: The lock stays closed (GCD > 1).

How They Solved It: The AI and the Human Team

This wasn't just a human scribbling on a napkin. The authors used MechMath, an AI agent designed to do math.

The Human-AI Partnership: The human authors built the AI agent. The agent then generated two things simultaneously:
- A natural language proof (like the one you are reading now, but written in standard math English).
- A formal proof written in a computer language called Lean.
The "Robot" Check: The Lean proof is like a set of instructions for a robot. The robot reads every single logical step. If the robot finds a gap or a mistake, it stops and says "Error." If it finishes without errors, the proof is 100% verified.
- This is important because human proofs can sometimes have tiny, invisible errors. The "robot proof" removes that doubt.
The Tools Used:
- Newton Interpolation: Think of this as a way to predict the shape of a curve by looking at the gaps between points. The team used this to show that any shared factor must be related to the number $k+1$ .
- Lucas' Theorem: This is a famous rule about how numbers behave when you look at them in different "bases" (like looking at a number in base 10 vs. base 2). The team used this to break the problem down into tiny, manageable "digit boxes."
- Digit Boxes: Imagine a grid of numbers. The team proved that if you try to shift this grid by a certain amount, the numbers will only stay inside the grid if the shift is "zero" (or a very specific type of zero). This helped them prove the final condition about the "tallest stack."

The Result: A New Entry in the Hall of Fame

The paper concludes with a victory lap:

They proved Ralf Stephan's guess (Conjecture 17) was correct.
They updated the Formal Conjectures project, a benchmark for AI and math.
Before this, the project had 96 unsolved problems and 4 solved ones.
After this paper, it has 95 unsolved and 5 solved.

Summary in One Sentence

This paper uses a team of humans and an AI to prove a long-standing guess about when a specific group of numbers shares no common factors, using a "tallest tower" rule and verifying the result with a computer-checkable robot proof.

Technical Summary: A Greatest Common Divisor Criterion of Certain Binomial Coefficients

Problem Statement
The paper addresses a specific number-theoretic problem concerning the greatest common divisor (gcd) of a selected family of binomial coefficients. For an integer $k \ge 2$ , the authors define:
$D(k) = \gcd_{2 \le q \le k+1} \binom{qk}{k}$
The objective is to characterize the integers $k$ for which $D(k) = 1$ . This problem corresponds to the integer sequence OEIS A080170 and was previously formulated as Conjecture (17) in Ralf Stephan's collection Prove or Disprove: 100 Conjectures from the OEIS. The conjecture posits a criterion based on the prime-power factorization of $n = k + 1$ . Specifically, if $P$ is the largest exact prime-power component of $n$ (denoted $P = \text{ppart}(n)$ , where $p^a \parallel n$ ), the conjecture asserts that $D(k) = 1$ if and only if $n/P > P$ .

Methodology
The proof proceeds through a combination of classical number theory and combinatorial arguments, structured into several logical steps:

Prime Divisor Restriction: Using a finite-difference argument (Newton interpolation), the authors first establish that any prime divisor $p$ of $D(k)$ must divide $k+1$ (i.e., $p \mid n$ ). This reduces the problem to analyzing the divisibility of $D(k)$ by primes dividing $n$ .
Lucas' Theorem Application: For a prime $p \mid n$ , the problem is reduced to a digit-wise analysis using Lucas' Theorem. The condition $\binom{N}{K} \not\equiv 0 \pmod p$ is translated into constraints on the base- $p$ digits of $N$ and $K$ .
Digit Box Analysis: The authors introduce the concept of a "digit box" $D_c$ , a set of integers defined by constraints on their base- $p$ digits relative to a bound $c$ . They prove a "Gap Bound" lemma regarding the spacing of elements in $D_c$ and a "No Nonzero Translation" lemma.
Stabilizer Theorem: A central result (Theorem 7) characterizes the multiplicative stabilizers of the digit box. It states that for a coprime multiplier $s$ , the condition $[sy]_P \in \{1, \dots, c\}$ for all non-zero $y \in D_c$ holds if and only if $s \equiv 1 \pmod{p^{L-\text{ord}_p(c)}}$ .
Zero-Run Lemma: This lemma connects a sequence of binomial divisibilities to a modular conclusion. If $\binom{m+tM}{m} \equiv 0 \pmod p$ for a range of $t$ , it implies a specific congruence for $M$ modulo a power of $p$ .
Primary Criterion Synthesis: Combining the above, the authors derive a $p$ -primary criterion: for $n = p^a b$ with $p \nmid b$ , $p \mid D(k)$ if and only if $b \le p^a$ . The final theorem follows by observing that $D(k)=1$ requires this inequality to hold for all prime-power components, which is equivalent to the condition involving the largest component $P$ .

Key Contributions

Proof of OEIS A080170: The paper provides a rigorous mathematical proof for the conjectural description of the sequence A080170, resolving a problem listed in Ralf Stephan's collection of 100 OEIS conjectures.
Formalization in Lean: A significant contribution is the complete formalization of the proof in the Lean 4 theorem prover. The natural-language proof and the Lean code were both generated by the "MechMath Agent Team," an AI agent developed by the authors.
Benchmark Advancement: The work updates the "Formal Conjectures" benchmark (specifically the subset FC100OpenSet1). The theorem gcdCondition_iff_primePowerCondition was previously an open research problem; its formalization and verification have changed the status of this subset from 96 open/4 solved to 95 open/5 solved.

Results
The main result is Theorem 1, which formally states:
Let $k \ge 2$ and $n = k + 1$ . Let $P = \text{ppart}(n)$ be the largest exact prime-power component of $n$ . Then:
$\gcd_{2 \le q \le k+1} \binom{qk}{k} = 1 \iff \frac{n}{P} > P$
The proof confirms that the gcd is 1 precisely when the largest prime-power factor of $k+1$ is strictly smaller than the cofactor of $k+1$ divided by that prime power.

Significance
The paper claims significance in two primary areas:

Mathematical Resolution: It settles a specific, open conjecture regarding binomial coefficients that had been recorded in the OEIS and Stephan's collection but lacked a proof.
Automated Theorem Proving: It serves as a test case for the "Formal Conjectures" project, demonstrating that an AI-driven agent (MechMath) can generate both a human-readable mathematical proof and a machine-checkable Lean formalization for a research-level problem. The successful acceptance of the Lean artifact into the benchmark repository validates the agent's capability to handle complex number-theoretic reasoning and formal verification.