MathDB

OEIS A080170 conjecture

For every integer k≥2k\ge 2, the binomial-coefficient gcd quantity D(k)D(k) specified in OEIS A080170 satisfies D(k)=1D(k)=1 if and only if k+1ppart⁡(k+1)>ppart⁡(k+1)\frac{k+1}{\operatorname{ppart}(k+1)}>\operatorname{ppart}(k+1), where ppart⁡(n)=max⁡{pa:p is prime and pa∥n}\operatorname{ppart}(n)=\max\{p^a:p\text{ is prime and }p^a\mathrel{\|}n\} is the largest exact prime-power component of nn.

References

Primary source

GitHub

Additional references

formal-mathematicsnumber-theory
Posted

Progress summary

Refreshed
Claimed solved

A June 2026 proof checked by computer in Lean resolves the conjecture, with no later error or challenge found.

OEIS A080170 conjectures an equivalence between a gcd condition on binomial coefficients and a condition involving the largest exact prime-power component of k+1k+1. The June 2026 preprint identifies this as conjecture (17) in Ralf Stephan’s collection and claims a proof for k≥2k \ge 2.

June 2026 formal resolution

The preprint proves D(k)=1⟺(k+1)/ppart⁡(k+1)>ppart⁡(k+1)D(k)=1 \Longleftrightarrow (k+1)/\operatorname{ppart}(k+1)>\operatorname{ppart}(k+1), using finite differences, Lucas’ theorem, and base-pp arguments. The proof and Lean formalization are attributed to the MechMath Agent Team; the pinned source has no sorry, and the Formal Conjectures entry is marked research solved. No counterexample, error report, withdrawal, or retraction was found.

Current status (as of August 2026): The conjecture is resolved by a machine-checked Lean formalization, while the associated mathematical paper remains a preprint rather than a peer-reviewed publication.

Sources

Solutions 0

No solutions have been posted yet.