Integral factorial ratios

DefinitionProduct of scaled factorials#✓fully proved

For a list \(L\) of natural numbers and a natural number \(n\), the product of scaled factorials of \(L\) at \(n\) is \(\prod_{a \in L} (an)!\), the product of the factorials \((an)!\) over the entries \(a\) of \(L\), counted with multiplicity; for the empty list it is \(1\).

def factorialProd (L : List ℕ) (n : ℕ) : ℕ :=
  (L.map fun a => Nat.factorial (a * n)).prod

Used by 9

Used byScaled factorial products at index zero divide · Scaled factorial product at index zero · Integral factorial ratio · The central binomial factorial ratio is integral · Characterization of integral factorial ratios · Permuting the numerator of an integral factorial ratio · Permuting the denominator of an integral factorial ratio · Equal tuples form an integral factorial ratio · Equal singletons form an integral factorial ratio

DefinitionIntegral factorial ratio#✓fully proved

For lists \(A = (a_1, \dots, a_k)\) and \(B = (b_1, \dots, b_l)\) of natural numbers, the pair \((A, B)\) is an integral factorial ratio when every \(a_i\) and every \(b_j\) is positive, \(a_1 + \dots + a_k = b_1 + \dots + b_l\), and for every natural number \(n\) the product \((b_1 n)! \cdots (b_l n)!\) divides \((a_1 n)! \cdots (a_k n)!\); equivalently, the quotient \(\frac{(a_1 n)! \cdots (a_k n)!}{(b_1 n)! \cdots (b_l n)!}\) is a natural number.

def IsIntegralFactorialRatio (A B : List ℕ) : Prop :=
  (∀ a ∈ A, 0 < a) ∧ (∀ b ∈ B, 0 < b) ∧ A.sum = B.sum ∧
    ∀ n : ℕ, factorialProd B n ∣ factorialProd A n

Sources

• K. Soundararajan, Integral factorial ratios (arXiv 1901.05133).

Uses 1 · Used by 7

Statement usesProduct of scaled factorials

Used byThe central binomial factorial ratio is integral · Characterization of integral factorial ratios · Integral factorial ratios are invariant under permutation · Permuting the numerator of an integral factorial ratio · Permuting the denominator of an integral factorial ratio · Equal tuples form an integral factorial ratio · Equal singletons form an integral factorial ratio

TheoremScaled factorial product at index zero#✓fully proved

For every list \(L\) of natural numbers, \(\prod_{a \in L} (a \cdot 0)! = 1\), since every factor equals \(0! = 1\).

theorem factorialProd_zero (L : List ℕ) : factorialProd L 0 = 1

Uses 1 · Used by 1

Statement usesProduct of scaled factorials

Used byScaled factorial products at index zero divide

TheoremScaled factorial products at index zero divide#✓fully proved

For all lists \(A\) and \(B\) of natural numbers, \(\prod_{b \in B} (b \cdot 0)!\) divides \(\prod_{a \in A} (a \cdot 0)!\), since both products equal \(1\).

theorem factorialProd_dvd_zero (A B : List ℕ) :
    factorialProd B 0 ∣ factorialProd A 0

Uses 2

Statement usesProduct of scaled factorials

Proof usesScaled factorial product at index zero

TheoremCharacterization of integral factorial ratios#✓fully proved

For lists \(A\) and \(B\) of natural numbers, \((A, B)\) is an integral factorial ratio if and only if every entry of \(A\) is positive, every entry of \(B\) is positive, the entries of \(A\) and the entries of \(B\) have the same sum, and for every natural number \(n\) the product \(\prod_{b \in B} (bn)!\) divides \(\prod_{a \in A} (an)!\).

theorem isIntegralFactorialRatio_iff (A B : List ℕ) :
    IsIntegralFactorialRatio A B ↔
      (∀ a ∈ A, 0 < a) ∧ (∀ b ∈ B, 0 < b) ∧ A.sum = B.sum ∧
        ∀ n : ℕ, factorialProd B n ∣ factorialProd A n

Uses 2

Statement usesIntegral factorial ratio · Product of scaled factorials

TheoremPermuting the numerator of an integral factorial ratio#✓fully proved

Let \(A\), \(A'\) and \(B\) be lists of natural numbers such that \(A'\) is a permutation of \(A\). If \((A, B)\) is an integral factorial ratio, then so is \((A', B)\).

theorem isIntegralFactorialRatio_perm_left {A A' B : List ℕ}
    (hperm : List.Perm A A') (h : IsIntegralFactorialRatio A B) :
    IsIntegralFactorialRatio A' B

Uses 2 · Used by 1

Statement usesIntegral factorial ratio

Proof usesProduct of scaled factorials

Used byIntegral factorial ratios are invariant under permutation

TheoremPermuting the denominator of an integral factorial ratio#✓fully proved

Let \(A\), \(B\) and \(B'\) be lists of natural numbers such that \(B'\) is a permutation of \(B\). If \((A, B)\) is an integral factorial ratio, then so is \((A, B')\).

theorem isIntegralFactorialRatio_perm_right {A B B' : List ℕ}
    (hperm : List.Perm B B') (h : IsIntegralFactorialRatio A B) :
    IsIntegralFactorialRatio A B'

Uses 2 · Used by 1

Statement usesIntegral factorial ratio

Proof usesProduct of scaled factorials

Used byIntegral factorial ratios are invariant under permutation

TheoremIntegral factorial ratios are invariant under permutation#✓fully proved

Let \(A\), \(A'\), \(B\) and \(B'\) be lists of natural numbers such that \(A'\) is a permutation of \(A\) and \(B'\) is a permutation of \(B\). If \((A, B)\) is an integral factorial ratio, then so is \((A', B')\).

theorem isIntegralFactorialRatio_perm {A A' B B' : List ℕ}
    (hA : List.Perm A A') (hB : List.Perm B B') (h : IsIntegralFactorialRatio A B) :
    IsIntegralFactorialRatio A' B'

Uses 3

Statement usesIntegral factorial ratio

Proof usesPermuting the numerator of an integral factorial ratio · Permuting the denominator of an integral factorial ratio

TheoremEqual tuples form an integral factorial ratio#✓fully proved

If every entry of a list \(L\) of natural numbers is positive, then \((L, L)\) is an integral factorial ratio.

theorem isIntegralFactorialRatio_refl (L : List ℕ) (hpos : ∀ a ∈ L, 0 < a) :
    IsIntegralFactorialRatio L L

Uses 2

Statement usesIntegral factorial ratio

Proof usesProduct of scaled factorials

TheoremEqual singletons form an integral factorial ratio#✓fully proved

For every positive natural number \(c\), the one-entry tuples \((c)\) and \((c)\) form an integral factorial ratio.

theorem isIntegralFactorialRatio_singleton_self (c : ℕ) (hc : 0 < c) :
    IsIntegralFactorialRatio [c] [c]

Uses 2

Statement usesIntegral factorial ratio

Proof usesProduct of scaled factorials

TheoremThe central binomial factorial ratio is integral#✓fully proved

The tuples \((2)\) and \((1, 1)\) form an integral factorial ratio: their entries are positive, their sums agree (\(2 = 1 + 1\)), and for every natural number \(n\), \(n! \cdot n!\) divides \((2n)!\).

theorem isIntegralFactorialRatio_centralBinom :
    IsIntegralFactorialRatio [2] [1, 1]

Uses 2

Statement usesIntegral factorial ratio

Proof usesProduct of scaled factorials

DefinitionErdős Problem 728#✓fully proved

The proposition that there is a real number \(\delta > 0\) such that for every real number \(\varepsilon\) with \(0 < \varepsilon < \delta\) and all real numbers \(C > 0\) and \(C' > C\), there are natural numbers \(a\), \(b\) and \(n \ge 1\) with \(a > \varepsilon n\), \(b > \varepsilon n\), \(a! \, b! \mid n! \, (a + b - n)!\) and \(n + C \log n < a + b < n + C' \log n\).

def conjecture : Prop :=
  ∀ᶠ ε : ℝ in 𝓝[>] 0, ∀ C > (0 : ℝ), ∀ C' > C,
    ∃ a b n : ℕ,
      0 < n ∧
      ε * n < a ∧
      ε * n < b ∧
      a ! * b ! ∣ n ! * (a + b - n)! ∧
      a + b > n + C * Real.log n ∧
      a + b < n + C' * Real.log n

Used by 1

Used byErdős Problem 728 holds

TheoremErdős Problem 728 holds#●ready to prove

There is a real number \(\delta > 0\) such that for every real number \(\varepsilon\) with \(0 < \varepsilon < \delta\) and all real numbers \(C > 0\) and \(C' > C\), there are natural numbers \(a\), \(b\) and \(n \ge 1\) with \(a > \varepsilon n\), \(b > \varepsilon n\), \(a! \, b! \mid n! \, (a + b - n)!\) and \(n + C \log n < a + b < n + C' \log n\).

The statement was resolved in the affirmative by Barreto and ChatGPT-5.2.

public theorem_wanted conjecture_holds : conjecture

Sources

• N. Sothanaphan, Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proof, arXiv:2601.07421 (2026), https://arxiv.org/abs/2601.07421.

Uses 1

Statement usesErdős Problem 728

DefinitionErdős Problem 729#✓fully proved

The proposition that for every real number \(C > 0\) there is a natural number \(K \ge 3\) such that there are infinitely many triples \((a, b, n)\) of positive integers with \(a + b > n + C \log n\) for which no prime \(p > K\) divides the denominator of the rational number \(n! / (a! \, b!)\) in lowest terms.

def conjecture : Prop :=
  ∀ (C : ℝ) (_ : C > 0),
    ∃ K ≥ 3, Set.Infinite {T : ℕ × ℕ × ℕ |
      let (a, b, n) := T
      a > 0 ∧ b > 0 ∧ n > 0 ∧
      (a : ℝ) + b > n + C * Real.log n ∧
      ∀ p, p.Prime → p > K →
        padicValNat p ((n.factorial / (a.factorial * b.factorial) : ℚ).den) = 0}

Used by 1

Used byErdős Problem 729 holds

TheoremErdős Problem 729 holds#●ready to prove

For every real number \(C > 0\) there is a natural number \(K \ge 3\) such that there are infinitely many triples \((a, b, n)\) of positive integers with \(a + b > n + C \log n\) for which no prime \(p > K\) divides the denominator of the rational number \(n! / (a! \, b!)\) in lowest terms.

The statement was resolved in the affirmative by Barreto and Leeham.

public theorem_wanted conjecture_holds : conjecture

Sources

• External Lean proof of Erdős Problem 729, https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/v4.29.1/ErdosProblems/Erdos729.lean.

Uses 1

Statement usesErdős Problem 729

13 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.