Binomial GCD Criterion (OEIS A080170)

A complete, self-contained Lean 4 formalization of the main result of

A Proof of the OEIS A080170 Binomial GCD Criterion, MechMath Agent Team. arXiv: https://arxiv.org/abs/2606.22997

For k ≥ 2 and n = k + 1, the paper proves

D(k) = gcd_{2 ≤ q ≤ k+1} C(qk, k) = 1   ↔   n / ppart(n) > ppart(n),

where ppart(n) is the largest exact prime-power component p^a ∥ n.

Contents

• A080170.lean — the full formalization.

Every theorem and lemma is fully proved (no sorry). The two top-level theorems a080170 and gcdCondition_iff_primePowerCondition depend only on the standard axioms propext, Classical.choice, and Quot.sound.

Relation to formal-conjectures

The final section mirrors FormalConjectures/OEIS/80170.lean from google-deepmind/formal-conjectures: gcdCondition_iff_primePowerCondition resolves that conjecture statement (named OeisA80170.gcdCondition_iff_primePowerCondition upstream). A PR contributing this resolution upstream has been approved. Because that project is large and pinned to Mathlib 4.27, this self-contained file is maintained separately and verifies cleanly against Mathlib 4.29.1.

Building / checking

The file is a single module that does import Mathlib. To check it, drop it into any Lean 4 project whose lean-toolchain and Mathlib revision match Mathlib 4.29.1, then build:

lake env lean A080170.lean   # checks the single file
# or, if added to the package's import tree:
lake build