FormalConjectures.OEIS.«211417»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Integrality and supercongruences of the factorial ratio $\frac{(6n)! n!}{(3n)! (2n)!^2}$

Integral factorial ratio sequence: $$a(n) = \frac{(30n)! n!}{(15n)! (10n)! (6n)!}$$

References:

A211417

arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.

namespace OeisA211417

Integral factorial ratio sequence: $$a(n) = \frac{(30n)! n!}{(15n)! (10n)! (6n)!}$$

def a (n : ℕ) : ℕ :=
  (Nat.factorial (30 * n) * Nat.factorial n) /
  (Nat.factorial (15 * n) * Nat.factorial (10 * n) * Nat.factorial (6 * n))

open Nat Int Finset

def coprimeIndices (r : ℕ) : Finset ℕ :=
  (Finset.range (r + 1)).filter (fun i => 1 ≤ i ∧ Nat.gcd i 30 = 1)

The product term in the denominator of the general conjecture: $$\prod_{i = 1..r, i \text{ coprime to } 30} (30n - i)$$ We define this in ℤ to handle the $n=0$ case where $30n-i$ in the product might be negative.

def divisorProduct (n r : ℕ) : ℤ :=
  (coprimeIndices r).prod (fun i : ℕ => 30 * (n : ℤ) - (i : ℤ))

@[category test, AMS 11]
lemma a_0 : a 0 = 1 := by⊢ a 0 = 1 rflAll goals completed! 🐙

@[category test, AMS 11]
lemma a_1 : a 1 = 77636318760 := by⊢ a 1 = 77636318760 rflAll goals completed! 🐙

@[category test, AMS 11]
lemma a_2 : a 2 = 53837289804317953893960 := by⊢ a 2 = 53837289804317953893960 rflAll goals completed! 🐙

@[category test, AMS 11]
lemma a_3 : a 3 = 43880754270176401422739454033276880 := by⊢ a 3 = 43880754270176401422739454033276880 rflAll goals completed! 🐙

@[category test, AMS 11]
lemma a_4 : a 4 = 38113558705192522309151157825210540422513019720 := by⊢ a 4 = 38113558705192522309151157825210540422513019720 rflAll goals completed! 🐙

It appears that $a(n)/(30n - 1)$ is integral for all $n$ (checked up to $n = 1000$). - Peter Bala, Aug 28 2025

A formal proof has been found with the methods described in arxiv/2605.22763.

@[category research solved, AMS 11, formal_proof using formal_conjectures at
"https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/211417.wip.lean#L243"]
theorem thirty_mul_sub_one_dvd_a (n : ℕ) : (30 * (n : ℤ) - 1) ∣ (a n : ℤ) := byn:ℕ⊢ 30 * ↑n - 1 ∣ ↑(a n)
    sorryAll goals completed! 🐙

Conjecture: "7a(n)/(2n + 1) ... [is an] integer for all n (checked up to n = 1000)."

Peter Bala, Aug 28 2025

@[category research solved, AMS 11,
  formal_proof using lean4 at
    "https://github.com/KitaKen1/oeis-a211417/blob/cad1fb228b5b80573cab3eeb92c8be57fd73c506/lean/OeisA211417FC.lean#L866-L868"]
theorem seven_mul_a_dvd_two_mul_add_one (n : ℕ) :
    (2 * (n : ℤ) + 1) ∣ 7 * (a n : ℤ) := byn:ℕ⊢ 2 * ↑n + 1 ∣ 7 * ↑(a n)
  sorryAll goals completed! 🐙

Conjecture: "a(n)/(3*n + 1) ... [is an] integer for all n (checked up to n = 1000)."

Peter Bala, Aug 28 2025

@[category research solved, AMS 11,
  formal_proof using lean4 at
    "https://github.com/KitaKen1/oeis-a211417/blob/cad1fb228b5b80573cab3eeb92c8be57fd73c506/lean/OeisA211417FC.lean#L1173-L1175"]
theorem a_dvd_three_mul_add_one (n : ℕ) :
    (3 * (n : ℤ) + 1) ∣ (a n : ℤ) := byn:ℕ⊢ 3 * ↑n + 1 ∣ ↑(a n)
  sorryAll goals completed! 🐙

Conjecture: "a(n)/(5*n + 1) ... [is an] integer for all n (checked up to n = 1000)."

Peter Bala, Aug 28 2025

@[category research solved, AMS 11,
  formal_proof using lean4 at
    "https://github.com/KitaKen1/oeis-a211417/blob/cad1fb228b5b80573cab3eeb92c8be57fd73c506/lean/OeisA211417FC.lean#L1446-L1448"]
theorem a_dvd_five_mul_add_one (n : ℕ) :
    (5 * (n : ℤ) + 1) ∣ (a n : ℤ) := byn:ℕ⊢ 5 * ↑n + 1 ∣ ↑(a n)
  sorryAll goals completed! 🐙

Conjecture: "42a(n)/((2n + 1)(3n + 1)(5n + 1)) [is an] integer for all n (checked up to n = 1000)." - Peter Bala, Aug 28 2025

@[category research solved, AMS 11,
  formal_proof using lean4 at
    "https://github.com/KitaKen1/oeis-a211417/blob/cad1fb228b5b80573cab3eeb92c8be57fd73c506/lean/OeisA211417FC.lean#L1514-L1524"]
theorem forty_two_mul_a_dvd_product (n : ℕ) :
    ((2 * (n : ℤ) + 1) * (3 * (n : ℤ) + 1) * (5 * (n : ℤ) + 1)) ∣
      42 * (a n : ℤ) := byn:ℕ⊢ (2 * ↑n + 1) * (3 * ↑n + 1) * (5 * ↑n + 1) ∣ 42 * ↑(a n)
  sorryAll goals completed! 🐙

Conjecture: "More generally, for r >= 1, we conjecture that there exists a constant D(r) such that D(r)a(n)/Product_{i = 1..r, i coprime to 30} (30n - i) is integral for all n."

Peter Bala, Aug 28 2025

This generalizes thirty_mul_sub_one_dvd_a (the $r = 1$ case where $D(1) = 1$).

Proof sketch (kernel-checked development at the formal_proof permalink below, which proves the non-vacuous form with the explicit positive witness $D = (r!)^{r^2}$): Legendre-valuation analysis of the Landau step function $\Delta(x) = \lfloor 30x \rfloor + \lfloor x \rfloor - \lfloor 15x \rfloor - \lfloor 10x \rfloor - \lfloor 6x \rfloor$, whose values lie in ${0, 1}$. Three ingredients: a unit-class rigidity lemma ($\Delta_c = 1$ for every unit class $c$ modulo $30$), a witness-uniqueness bound for prime powers $p^k > r$ (at most one factor of the divisor product is divisible by $p^k$), and a uniform low-layer budget for $p^k \le r$ absorbed by the witness constant.

@[category research solved, AMS 11, formal_proof using formal_conjectures at
"https://github.com/chy4pro/formal-conjectures/blob/fbc6706451b0e80787580d91ee6c252c121e0165/FormalConjectures/OEIS/211417.lean#L651"]
theorem general_divisibility (r : ℕ) (hr : 1 ≤ r) :
    ∃ D : ℤ, 0 < D ∧ ∀ n : ℕ, (divisorProduct n r) ∣ (D * (a n : ℤ)) := byr:ℕhr:1 ≤ r⊢ ∃ D, 0 < D ∧ ∀ (n : ℕ), divisorProduct n r ∣ D * ↑(a n)
  sorryAll goals completed! 🐙

Supercongruence: "a(p^k) == a(p^(k-1)) ( mod p^(3*k) ) for any prime p >= 5 and any positive integer k." - Peter Bala, Jan 24 2020

More generally, "the congruences a(np^k) == a(np^(k-1)) ( mod p^(3*k) ) may hold for any prime p >= 5 and any positive integers n and k."

@[category research open, AMS 11]
theorem supercongruence (p k : ℕ) (hp : p.Prime) (hp5 : 5 ≤ p) (hk : 0 < k) :
    (p : ℤ) ^ (3 * k) ∣ ((a (p ^ k) : ℤ) - (a (p ^ (k - 1)) : ℤ)) := byp:ℕk:ℕhp:Nat.Prime php5:5 ≤ phk:0 < k⊢ ↑p ^ (3 * k) ∣ ↑(a (p ^ k)) - ↑(a (p ^ (k - 1)))
  sorryAll goals completed! 🐙

end OeisA211417