Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

bibkey: kitamura2026a211417 authors: Kenta Kitamura year: 2026 title: “Kernel-checked Lean proofs of the four OEIS A211417 divisibility conjectures” doi: null url: https://github.com/KitaKen1/oeis-a211417/blob/cad1fb228b5b80573cab3eeb92c8be57fd73c506/lean/OeisA211417FC.lean claim: “For a(n) = (30n)! n! / ((15n)! (10n)! (6n)!), the divisibilities (2n+1) | 7 a(n), (3n+1) | a(n), (5n+1) | a(n) and (2n+1)(3n+1)(5n+1) | 42 a(n) hold for every natural n; all four are kernel-checked Lean 4 theorems with axiom closure {propext, Classical.choice, Quot.sound}.” strata_touched:

  • D5/S3/Arith/FactorialRatio/BalaChebyshevThreeDivisibility
  • D5/S3/Arith/FactorialRatio/BalaChebyshevFiveDivisibility license: citation-only triage: anchor

Kernel-checked Lean proofs of the four OEIS A211417 divisibility conjectures

Verified locator

https://github.com/KitaKen1/oeis-a211417/blob/cad1fb228b5b80573cab3eeb92c8be57fd73c506/lean/OeisA211417FC.lean

The immutable file lean/OeisA211417FC.lean at commit cad1fb228b5b80573cab3eeb92c8be57fd73c506 of the repository KitaKen1/oeis-a211417 contains the four target theorems, among them seven_mul_a_dvd_two_mul_add_one_nat. They are recorded as solved in google-deepmind/formal-conjectures, pull request #5010 (“Mark four OEIS A211417 divisibility conjectures as solved”, merged 2026-08-16), file FormalConjectures/OEIS/211417.lean.

Source statement

Peter Bala’s comment on OEIS A211417 (2025-08-28) reads:

Conjectures: 7a(n)/(2n + 1), a(n)/(3n + 1), a(n)/(5n + 1) and 42a(n)/((2n + 1)(3n + 1)(5n + 1)) are integers for all n

The linked Lean development proves exactly these four statements. #print axioms on the four targets reports only propext, Classical.choice and Quot.sound.

Correspondence to this repository

D5/S3/Arith/FactorialRatio/BalaChebyshevThreeDivisibility.bala_three_integrality and D5/S3/Arith/FactorialRatio/BalaChebyshevFiveDivisibility.bala_five_integrality state the 3n+1 and 5n+1 cases in division-free form. Both are therefore literature-attested: the statements were established publicly, in Lean, before the corresponding modules were frozen here. The proofs in this repository are independent (Legendre-valuation accounting with an exceptional-scale contribution) and the frozen statements are unchanged by this attestation.

Boundaries

The 2n+1 case and the 42 a(n) product case have no frozen module here. The 30n−1 divisibility listed separately in the OEIS entry is not part of Kitamura’s four theorems.