The Guo–Krattenthaler divisibilities (6n−1) ∣ C(12n,3n) and (6n−1) ∣ C(12n,4n) hold for every n = 1..8, and (66n−1) ∣ C(330n,88n) at n = 1 — kernel-attested instances of the all-n theorems of Guo & Krattenthaler (2014)

Enuntiatio — the claim

The Guo–Krattenthaler divisibilities (6n−1) ∣ C(12n,3n) and (6n−1) ∣ C(12n,4n) hold for every n = 1..8, and (66n−1) ∣ C(330n,88n) at n = 1 — kernel-attested instances of the all-n theorems of Guo & Krattenthaler (2014)

Refuted by an n between 1 and 8 with (6n−1) ∤ C(12n,3n) or (6n−1) ∤ C(12n,4n), or 65 ∤ C(330,88)

Expressio — the formal statement

import Mathlib.Tactic

set_option maxRecDepth 8000

theorem gk_divisibilities : (∀ n < 8, (6*(n+1) - 1) ∣ Nat.choose (12*(n+1)) (3*(n+1)) ∧ (6*(n+1) - 1) ∣ Nat.choose (12*(n+1)) (4*(n+1))) ∧ (65 : ℕ) ∣ Nat.choose 330 88

Demonstratio — the kernel-checked proof

by decide