Pith. sign in

REVIEW 1 minor 1 cited by

Binomial gcd D(k) equals 1 exactly when n/P exceeds P, with P the largest prime-power divisor of n = k+1.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.3

2026-06-26 07:23 UTC pith:IW3Q4Z7E

load-bearing objection The paper proves and Lean-formalizes a narrow binomial gcd criterion that was already conjectured in OEIS and Stephan's list.

arxiv 2606.22997 v1 pith:IW3Q4Z7E submitted 2026-06-22 math.NT cs.LO

A Greatest Common Divisor Criterion of Certain Binomial Coefficients

Dakai Guo , Ruichen Qiu , Yichuan Cao , Ruyong Feng , Xiao-Shan Gao This is my paper
classification math.NT cs.LO
keywords binomial coefficientsgreatest common divisorprime powersnumber theoryOEIS A080170formal verificationLean theorem prover
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proves an exact criterion for when a specific family of binomial coefficients shares no common divisor larger than one. Define D(k) as the gcd of binom(qk, k) over q from 2 to k+1, and let n equal k+1. If P is the largest prime power exactly dividing n, then D(k) equals one if and only if n/P is greater than P. This settles a recorded OEIS conjecture and is accompanied by a complete Lean formalization of both the statement and its proof. A reader cares because the condition depends only on the prime factorization of n rather than direct computation of the binomials themselves.

Core claim

The paper proves that for k greater than or equal to 2, D(k) equals 1 if and only if n/P is greater than P, where D(k) is the gcd over q=2 to k+1 of binom(qk, k), n equals k+1, and P is the largest prime-power component exactly dividing n. Both the natural-language argument and its Lean encoding are supplied, with the formal artifact accepted into the Formal Conjectures project.

What carries the argument

The equivalence D(k)=1 ⇔ n/P > P, where P is the largest prime power exactly dividing n.

Load-bearing premise

The Lean formalization correctly encodes the natural-language statement of the criterion together with all intermediate lemmas.

What would settle it

Finding any integer k greater than or equal to 2 such that D(k) is greater than 1 yet n/P exceeds P, or D(k) equals 1 yet n/P does not exceed P, would falsify the claimed equivalence.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • The value of D(k) is completely determined by the prime factorization of n without evaluating any binomial coefficient.
  • The criterion holds for every integer k at least 2.
  • The result resolves conjecture (17) in Ralf Stephan's list of OEIS conjectures.
  • The Lean artifact provides a machine-checked verification that can be independently checked by the theorem-prover community.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same factorization test could be used to decide coprimality questions for other ranges of binomial coefficients without explicit gcd computation.
  • The existence of an elementary criterion suggests similar divisibility statements for binomial arrays may reduce to prime-power comparisons.
  • Computational checks for very large k become feasible once the prime factorization of n is known.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

0 major / 1 minor

Summary. The manuscript proves the binomial gcd criterion recorded as OEIS A080170 (also conjecture (17) in Stephan's list). For k≥2, D(k) is defined as the gcd of binom(qk,k) over 2≤q≤k+1, with n=k+1; if P is the largest prime-power exactly dividing n, then D(k)=1 if and only if n/P > P. Both a natural-language proof and a Lean formalization are provided, with the Lean artifact accepted into the independent Formal Conjectures project.

Significance. If the result holds, it resolves a recorded OEIS conjecture. The acceptance of the Lean formalization into Formal Conjectures supplies independent machine-checked verification of the proof, which is a clear strength of the work and raises the evidential bar above a conventional pen-and-paper argument.

minor comments (1)
  1. [Abstract] Abstract: the description of the Lean artifact could include a one-sentence indication of the main formalized lemmas or the structure of the proof (e.g., induction on the prime-power factorization) to orient readers who will not immediately consult the repository.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment and recommendation to accept the manuscript. The report correctly captures the main result and the value of the independent Lean verification.

Circularity Check

0 steps flagged

No circularity; external Lean formalization supplies independent verification of the criterion

full rationale

The paper states an external conjecture (OEIS A080170 / Stephan (17)), supplies a natural-language proof, and encodes the identical statement plus lemmas in Lean. The Lean artifact is machine-checked by the kernel and accepted into the independent Formal Conjectures project. No step reduces by definition, by fitting a parameter then relabeling it a prediction, or by a load-bearing self-citation whose justification is internal to the authors. The formalization therefore constitutes external evidence rather than a renaming or self-referential closure. The derivation chain is self-contained against the external benchmark.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Only the abstract is available, so the ledger records reliance on standard number-theoretic background rather than any new fitted constants or postulated objects.

axioms (1)
  • standard math Standard properties of binomial coefficients, primes, and the gcd operation on the integers
    Invoked throughout any proof of the stated criterion.

pith-pipeline@v0.9.1-grok · 5690 in / 1215 out tokens · 42890 ms · 2026-06-26T07:23:14.818355+00:00 · methodology

0 comments
read the original 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.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. MechMath Agent Team: LLM Driven Agents for Mathematical Research

    cs.AI 2026-07 conditional novelty 7.0 partial

    A decoupled multi-agent LLM system (Harness + KB/NL/FL provers) co-piloted solutions to 11 open math problems, some with Lean formalization.

Reference graph

Works this paper leans on

14 extracted references · 7 canonical work pages · cited by 1 Pith paper · 3 internal anchors

  1. [1]

    Brown, Jr

    Edgar H. Brown, Jr. and Franklin P . Peterson. Relations among characteristic classes. II.Annals of Mathematics, 81(2):356–363, 1965.https://doi.org/10.2307/1970620

    work page doi:10.2307/1970620 1965

  2. [2]

    Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics

    Moritz Firsching, Paul Lezeau, Simone Mercuri, Márton Zsombor Horváth, Yaël Dillies, Christian Sönne, Eric Wieser, Fred Zhang, Thomas Hubert, Blaise Agüera y Arcas, and Pushmeet Kohli. Formal conjectures: An open and evolving benchmark for verified discovery in mathematics.https://arxiv. org/abs/2605.13171, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  3. [3]

    The greatest common divisor of certain binomial coefficients.Comptes Rendus Mathe- matique, 354(8):756–761, 2016.https://doi.org/10.1016/j.crma.2016.06.001

    Shaofang Hong. The greatest common divisor of certain binomial coefficients.Comptes Rendus Mathe- matique, 354(8):756–761, 2016.https://doi.org/10.1016/j.crma.2016.06.001

    work page doi:10.1016/j.crma.2016.06.001 2016

  4. [4]

    Joris, C

    H. Joris, C. Oestreicher, and J. Steinig. The greatest common divisor of certain sets of binomial co- efficients.Journal of Number Theory, 21(1):101–119, 1985.https://doi.org/10.1016/0022-314X(85) 90013-7

    work page doi:10.1016/0022-314x(85 1985

  5. [5]

    On toric generators in the unitary and special unitary bordism rings.Algebraic & Geometric Topology, 16(5):2865–2893, 2016.https://doi.org/10.2140/agt.2016.16.2865

    Zhi Lü and Taras Panov. On toric generators in the unitary and special unitary bordism rings.Algebraic & Geometric Topology, 16(5):2865–2893, 2016.https://doi.org/10.2140/agt.2016.16.2865

    work page doi:10.2140/agt.2016.16.2865 2016

  6. [6]

    Édouard Lucas. Sur les congruences des nombres euleriens et des coefficients differentiels des fonc- tions trigonometriques, suivant un module premier.Bulletin de la Société Mathématique de France, 6: 49–54, 1878

  7. [7]

    On the greatest common divisor of binomial coefficients (n q), ( n 2q), ( n 3q),

    Cameron McTague. On the greatest common divisor of binomial coefficients (n q), ( n 2q), ( n 3q), . . ..The American Mathematical Monthly, 124(4):353–356, 2017. Also available ashttps://arxiv.org/abs/1510. 06696

    2017

  8. [8]

    MechMath Agent Team.https://mechmath.github.io/, 2026

    MechMath Agent Team Authors. MechMath Agent Team.https://mechmath.github.io/, 2026

    2026

  9. [9]

    Lucas' theorem: its generalizations, extensions and applications (1878--2014)

    Romeo Meštrovi´ c. Lucas’ theorem: its generalizations, extensions and applications (1878–2014). https://arxiv.org/abs/1409.3820, 2014

    work page internal anchor Pith review Pith/arXiv arXiv 2014

  10. [10]

    The on-line encyclopedia of integer sequences, A080170

    OEIS Foundation Inc. The on-line encyclopedia of integer sequences, A080170. Published electroni- cally athttps://oeis.org/A080170, 2026

    2026

  11. [11]

    B. Ram. Common factors ofn!/(m!(n−m)!) (m=1, 2, . . . ,n−1).Journal of the Indian Mathematical Club, 1:39–43, 1909. 12 Key Laboratory of Mathematics Mechanization MechMath Agent Team

    1909

  12. [12]

    N. J. A. Sloane. The on-line encyclopedia of integer sequences.Notices of the American Mathematical Society, 50:912–915, 2003. Also available ashttps://arxiv.org/abs/math/0312448

    work page internal anchor Pith review Pith/arXiv arXiv 2003

  13. [13]

    Prove or disprove

    Ralf Stephan. Prove or disprove. 100 conjectures from the OEIS.https://arxiv.org/abs/math/ 0409509, 2004

    2004

  14. [14]

    The formal conjectures repository.https://github.com/ google-deepmind/formal-conjectures, 2025

    The Formal Conjectures Authors. The formal conjectures repository.https://github.com/ google-deepmind/formal-conjectures, 2025. 13

    2025