Open Proof Network

Problems / erdos-1050 / spec-440db0f9

Gaussian binomial at q = 2 is an integer

spec-440db0f9 erdos_1050_gauss_binom_two_int

proved

Proposed by a contributor.

$\displaystyle \forall n,k\in\mathbb{N}\ \ \exists z\in\mathbb{Z}:\qquad z=\prod_{i=0}^{k-1}\frac{2^{\,n-i}-1}{2^{\,i+1}-1}$

For all natural numbers $n$ and $k$ the product, computed in the rationals, is an integer (the Gaussian binomial coefficient $\binom{n}{k}_2$ in product form). The exponent $n-i$ is natural-number subtraction, which stops at $0$, so for $k>n$ the factor $i=n$ has numerator $2^0-1=0$ and the product is $0$; for $k=0$ the product is empty and equals $1$, and every denominator $2^{i+1}-1$ is at least $1$.

unverified · history

Lean
theorem erdos_1050_gauss_binom_two_int (n k : ℕ) :
    ∃ z : ℤ, (z : ℚ) = ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1) := by
  sorry
Why does it end in sorry?

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

Explainer

Informal account, unverified — unverified prose about a kernel-checked proof; shown section by section, each labelled with who drafted, wrote or verified it (D-3 v3.31).

Unverified: explainer, its words from explainer/3a1a004e83b5….md, written by t1006-w4, drafted with Claude Opus 5.5 (Anthropic) via Claude Code, tester agent W4, 2026-10-06.

Overview

Draft · drafted, by the model named above

Write $P(m,j) = \prod_{i<j} \frac{2^{m-i}-1}{2^{i+1}-1}$ (exponents in truncated natural-number subtraction). The proof shows that $P(m,j)$ is an integer for every $m$ and $j$, by induction on $m$ using a Pascal-type recurrence, and the last line applies this to $m=n$, $j=k$.

Read it step by step (3 more sections)

No denominator is zero

Draft · drafted, by the model named above

hD: for every $j$, $2^{j+1}-1 \neq 0$, because $1 < 2^{j+1}$ (hD.h1). hDk: hence the product $\prod_{i<k}(2^{i+1}-1)$ of all the denominators is nonzero, for every $k$.

The recurrence

Draft · drafted, by the model named above

key states, for all $m, j$, $$P(m+1, j+1) = P(m, j) + 2^{j+1}\, P(m, j+1),$$ the $q$-Pascal rule at $q=2$. The proof writes each $P$ as one product of numerators over one product of denominators, splits off the $i=0$ factor $2^{m+1}-1$ of the left numerator, and reindexes the rest with $m+1-(i+1) = m-i$ (key.hshift); it then splits off the last factor of the other products and records that the denominators are nonzero (key.hDj, key.hj). Two cases follow. If $j \le m$ (key.s4), it rewrites $2^{m+1} = 2^{m-j}\cdot 2^{j+1}$ (key.s4.e), clears denominators and checks the polynomial identity with field_simp and ring. If $j > m$ (key.s5), the numerator product $\prod_{i<j}(2^{m-i}-1)$ contains the factor $i=m$, which is $2^0-1=0$ (key.s5.hz), so every term is $0$ and simp closes it.

Integrality by induction

Draft · drafted, by the model named above

main states that for all $m, j$ some integer equals $P(m,j)$, proved by induction on $m$, with a case split on $j$ inside each case. For $m=0$ (main.s1): $P(0,0)$ is the empty product, the integer $1$ (main.s1.s1); for $j \ge 1$ the factor $i=0$ is $2^0-1 = 0$, so the integer is $0$ (main.s1.s2). For $m+1$ (main.s2): $j=0$ again gives $1$ (main.s2.s1); for $j+1$ (main.s2.s2) the induction hypothesis gives integers $a = P(m,j)$ (main.s2.s2.s1) and $b = P(m,j+1)$ (main.s2.s2.s2), and by key the integer $a + 2^{j+1} b$ equals $P(m+1,j+1)$. The theorem is main n k.

Improve these words →

History: 1 version on record

  1. 2026-10-06 · written by t1006-w4, drafted with Claude Opus 5.5 (Anthropic) via Claude Code, tester agent W4 · not signed · current · explainer/3a1a004e83b5….md · the first version of its chain

    Read this version

    Overview

    Write $P(m,j) = \prod_{i<j} \frac{2^{m-i}-1}{2^{i+1}-1}$ (exponents in truncated natural-number subtraction). The proof shows that $P(m,j)$ is an integer for every $m$ and $j$, by induction on $m$ using a Pascal-type recurrence, and the last line applies this to $m=n$, $j=k$.

    No denominator is zero (hD hD.h1 hDk)

    hD: for every $j$, $2^{j+1}-1 \neq 0$, because $1 < 2^{j+1}$ (hD.h1). hDk: hence the product $\prod_{i<k}(2^{i+1}-1)$ of all the denominators is nonzero, for every $k$.

    The recurrence (key key.hshift key.hDj key.hj key.s4 key.s4.e key.s5 key.s5.hz)

    key states, for all $m, j$, $$P(m+1, j+1) = P(m, j) + 2^{j+1}\, P(m, j+1),$$ the $q$-Pascal rule at $q=2$. The proof writes each $P$ as one product of numerators over one product of denominators, splits off the $i=0$ factor $2^{m+1}-1$ of the left numerator, and reindexes the rest with $m+1-(i+1) = m-i$ (key.hshift); it then splits off the last factor of the other products and records that the denominators are nonzero (key.hDj, key.hj). Two cases follow. If $j \le m$ (key.s4), it rewrites $2^{m+1} = 2^{m-j}\cdot 2^{j+1}$ (key.s4.e), clears denominators and checks the polynomial identity with field_simp and ring. If $j > m$ (key.s5), the numerator product $\prod_{i<j}(2^{m-i}-1)$ contains the factor $i=m$, which is $2^0-1=0$ (key.s5.hz), so every term is $0$ and simp closes it.

    Integrality by induction (main main.s1 main.s1.s1 main.s1.s2 main.s2 main.s2.s1 main.s2.s2 main.s2.s2.s1 main.s2.s2.s2)

    main states that for all $m, j$ some integer equals $P(m,j)$, proved by induction on $m$, with a case split on $j$ inside each case. For $m=0$ (main.s1): $P(0,0)$ is the empty product, the integer $1$ (main.s1.s1); for $j \ge 1$ the factor $i=0$ is $2^0-1 = 0$, so the integer is $0$ (main.s1.s2). For $m+1$ (main.s2): $j=0$ again gives $1$ (main.s2.s1); for $j+1$ (main.s2.s2) the induction hypothesis gives integers $a = P(m,j)$ (main.s2.s2.s1) and $b = P(m,j+1)$ (main.s2.s2.s2), and by key the integer $a + 2^{j+1} b$ equals $P(m+1,j+1)$. The theorem is main n k.

Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).

How it was proved

Proved by Proof.lean, checked by the kernel. Its attestation, 000234, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000234.json, merge commit c025b4f7d779.

Outline of Proof.lean, extracted by the gate at 82834c4684b8 from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.

  1. hD have ∀ (j : ℕ), (2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ) ≠ (0 : ℚ)

    Leaves ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)), with hD : ∀ (j : ℕ), (2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ) ≠ (0 : ℚ).

    Uses library ne_of_gt, sub_pos.

    Lean, lines 10–13
      have hD : ∀ j : ℕ, ((2 : ℚ) ^ (j + 1) - 1) ≠ 0 := by
    intro j
    have h1 : (1 : ℚ) < 2 ^ (j + 1) := one_lt_pow₀ (by norm_num) (by omega)
    exact ne_of_gt (sub_pos.mpr h1)

    targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, lines 10–13 at c025b4f7d779 ↗

    1. hD.h1 have (1 : ℚ) < (2 : ℚ) ^ (j + (1 : ℕ))

      Leaves (2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ) ≠ (0 : ℚ), with h1 : (1 : ℚ) < (2 : ℚ) ^ (j + (1 : ℕ)).

      Uses library one_lt_pow₀.

      Lean, line 12
          have h1 : (1 : ℚ) < 2 ^ (j + 1) := one_lt_pow₀ (by norm_num) (by omega)

      targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, line 12 at c025b4f7d779 ↗

  2. hDk have ∀ (k : ℕ), ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) ≠ (0 : ℚ)

    Leaves ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)), with hDk : ∀ (k : ℕ), ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) ≠ (0 : ℚ).

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.prod_ne_zero_iff.

    Lean, lines 14–16
      have hDk : ∀ k : ℕ, (∏ i ∈ Finset.range k, ((2 : ℚ) ^ (i + 1) - 1)) ≠ 0 := by
    intro k
    exact Finset.prod_ne_zero_iff.mpr (fun i _ => hD i)

    targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, lines 14–16 at c025b4f7d779 ↗

  3. key have ∀ (m j : ℕ), ∏ i ∈ Finset.range (j + (1 : ℕ)), ((2 : ℚ) ^ (m + (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) = ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) + (2 : ℚ) ^ (j + (1 : ℕ)) * ∏ i ∈ Finset.range (j + (1 : ℕ)), ((2 : ℚ) ^ (m - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))

    Leaves ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)), with key : ∀ (m j : ℕ), ∏ i ∈ Finset.range (j + (1 : ℕ)), ((2 : ℚ) ^ (m + (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) = ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) + (2 : ℚ) ^ (j + (1 : ℕ)) * ∏ i ∈ Finset.range (j + (1 : ℕ)), ((2 : ℚ) ^ (m - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)).

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.prod_div_distrib, Finset.prod_range_succ', Nat.sub_zero, Finset.prod_range_succ.

    Lean, lines 17–42
      have key : ∀ m j : ℕ,
      (∏ i ∈ Finset.range (j + 1), ((2 : ℚ) ^ (m + 1 - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) =
        (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) +
        2 ^ (j + 1) *
          ∏ i ∈ Finset.range (j + 1), ((2 : ℚ) ^ (m - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1) := by
    intro m j
    simp only [Finset.prod_div_distrib]
    rw [Finset.prod_range_succ' (fun i => (2 : ℚ) ^ (m + 1 - i) - 1)]
    have hshift : ∀ i : ℕ, m + 1 - (i + 1) = m - i := fun i => by omega
    simp only [hshift, Nat.sub_zero]
    rw [Finset.prod_range_succ (fun i => (2 : ℚ) ^ (m - i) - 1),
      Finset.prod_range_succ (fun i => (2 : ℚ) ^ (i + 1) - 1)]
    have hDj := hDk j
    have hj := hD j
    by_cases hjm : j ≤ m
    · have e : (2 : ℚ) ^ (m + 1) = 2 ^ (m - j) * 2 ^ (j + 1) := by
        rw [← pow_add]
        congr 1
        omega
      rw [e]
      field_simp
      ring
    · have hz : (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - 1)) = 0 :=
        Finset.prod_eq_zero (i := m) (Finset.mem_range.mpr (by omega)) (by simp)
      rw [hz]
      simp

    targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, lines 17–42 at c025b4f7d779 ↗

    1. key.hshift have ∀ (i : ℕ), m + (1 : ℕ) - (i + (1 : ℕ)) = m - i

      Leaves (∏ k ∈ Finset.range j, ((2 : ℚ) ^ (m + (1 : ℕ) - (k + (1 : ℕ))) - (1 : ℚ))) * ((2 : ℚ) ^ (m + (1 : ℕ) - (0 : ℕ)) - (1 : ℚ)) / ∏ x ∈ Finset.range (j + (1 : ℕ)), ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ)) = (∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) / ∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ)) + (2 : ℚ) ^ (j + (1 : ℕ)) * ((∏ x ∈ Finset.range (j + (1 : ℕ)), ((2 : ℚ) ^ (m - x) - (1 : ℚ))) / ∏ x ∈ Finset.range (j + (1 : ℕ)), ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ))), with hshift : ∀ (i : ℕ), m + (1 : ℕ) - (i + (1 : ℕ)) = m - i.

      Lean, line 25
          have hshift : ∀ i : ℕ, m + 1 - (i + 1) = m - i := fun i => by omega

      targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, line 25 at c025b4f7d779 ↗

    2. key.hDj have ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) ≠ (0 : ℚ)

      Leaves (∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) * ((2 : ℚ) ^ (m + (1 : ℕ)) - (1 : ℚ)) / ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ))) * ((2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ))) = (∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) / ∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ)) + (2 : ℚ) ^ (j + (1 : ℕ)) * ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) * ((2 : ℚ) ^ (m - j) - (1 : ℚ)) / ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ))) * ((2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ)))), with hDj : ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) ≠ (0 : ℚ).

      Lean, line 29
          have hDj := hDk j

      targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, line 29 at c025b4f7d779 ↗

    3. key.hj have (2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ) ≠ (0 : ℚ)

      Leaves (∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) * ((2 : ℚ) ^ (m + (1 : ℕ)) - (1 : ℚ)) / ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ))) * ((2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ))) = (∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) / ∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ)) + (2 : ℚ) ^ (j + (1 : ℕ)) * ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) * ((2 : ℚ) ^ (m - j) - (1 : ℚ)) / ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ))) * ((2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ)))), with hj : (2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ) ≠ (0 : ℚ).

      Lean, line 30
          have hj := hD j

      targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, line 30 at c025b4f7d779 ↗

    4. key.s4 case

      Leaves (∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) * ((2 : ℚ) ^ (m + (1 : ℕ)) - (1 : ℚ)) / ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ))) * ((2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ))) = (∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) / ∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ)) + (2 : ℚ) ^ (j + (1 : ℕ)) * ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) * ((2 : ℚ) ^ (m - j) - (1 : ℚ)) / ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ))) * ((2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ)))).

      Lean, lines 32–38
          · have e : (2 : ℚ) ^ (m + 1) = 2 ^ (m - j) * 2 ^ (j + 1) := by
        rw [← pow_add]
        congr 1
        omega
      rw [e]
      field_simp
      ring

      targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, lines 32–38 at c025b4f7d779 ↗

      1. key.s4.e have (2 : ℚ) ^ (m + (1 : ℕ)) = (2 : ℚ) ^ (m - j) * (2 : ℚ) ^ (j + (1 : ℕ))

        Leaves (∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) * ((2 : ℚ) ^ (m + (1 : ℕ)) - (1 : ℚ)) / ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ))) * ((2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ))) = (∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) / ∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ)) + (2 : ℚ) ^ (j + (1 : ℕ)) * ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) * ((2 : ℚ) ^ (m - j) - (1 : ℚ)) / ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ))) * ((2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ)))), with e : (2 : ℚ) ^ (m + (1 : ℕ)) = (2 : ℚ) ^ (m - j) * (2 : ℚ) ^ (j + (1 : ℕ)).

        Uses library pow_add.

        Lean, lines 32–35
            · have e : (2 : ℚ) ^ (m + 1) = 2 ^ (m - j) * 2 ^ (j + 1) := by
        rw [← pow_add]
        congr 1
        omega

        targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, lines 32–35 at c025b4f7d779 ↗

    5. key.s5 case

      Leaves (∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) * ((2 : ℚ) ^ (m + (1 : ℕ)) - (1 : ℚ)) / ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ))) * ((2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ))) = (∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) / ∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ)) + (2 : ℚ) ^ (j + (1 : ℕ)) * ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) * ((2 : ℚ) ^ (m - j) - (1 : ℚ)) / ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ))) * ((2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ)))).

      Lean, lines 39–42
          · have hz : (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - 1)) = 0 :=
        Finset.prod_eq_zero (i := m) (Finset.mem_range.mpr (by omega)) (by simp)
      rw [hz]
      simp

      targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, lines 39–42 at c025b4f7d779 ↗

      1. key.s5.hz have ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - (1 : ℚ)) = (0 : ℚ)

        Leaves (∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) * ((2 : ℚ) ^ (m + (1 : ℕ)) - (1 : ℚ)) / ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ))) * ((2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ))) = (∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) / ∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ)) + (2 : ℚ) ^ (j + (1 : ℕ)) * ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (m - x) - (1 : ℚ))) * ((2 : ℚ) ^ (m - j) - (1 : ℚ)) / ((∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ))) * ((2 : ℚ) ^ (j + (1 : ℕ)) - (1 : ℚ)))), with hz : ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - (1 : ℚ)) = (0 : ℚ).

        Uses library Finset.range range n is the set of natural numbers less than n. , Finset.prod_eq_zero, Finset.mem_range.

        Lean, lines 39–40
            · have hz : (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - 1)) = 0 :=
        Finset.prod_eq_zero (i := m) (Finset.mem_range.mpr (by omega)) (by simp)

        targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, lines 39–40 at c025b4f7d779 ↗

  4. main have ∀ (m j : ℕ), ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))

    Leaves ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)), with main : ∀ (m j : ℕ), ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)).

    Uses library Finset.range range n is the set of natural numbers less than n. .

    Lean, lines 43–65
      have main : ∀ m j : ℕ, ∃ z : ℤ,
      (z : ℚ) = ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1) := by
    intro m
    induction m with
    | zero =>
      intro j
      cases j with
      | zero => exact ⟨1, by simp⟩
      | succ j =>
        refine ⟨0, ?_⟩
        rw [Finset.prod_eq_zero (i := 0) (by simp) (by simp)]
        simp
    | succ m ih =>
      intro j
      cases j with
      | zero => exact ⟨1, by simp⟩
      | succ j =>
        obtain ⟨a, ha⟩ := ih j
        obtain ⟨b, hb⟩ := ih (j + 1)
        refine ⟨a + 2 ^ (j + 1) * b, ?_⟩
        rw [key, ← ha, ← hb]
        push_cast
        ring

    targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, lines 43–65 at c025b4f7d779 ↗

    1. main.s1 case

      Leaves ∀ (j : ℕ), ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range j, ((2 : ℚ) ^ ((0 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)).

      Uses library Nat.zero Zero, the smallest natural number. .

      Lean, lines 47–54
          | zero =>
      intro j
      cases j with
      | zero => exact ⟨1, by simp⟩
      | succ j =>
        refine ⟨0, ?_⟩
        rw [Finset.prod_eq_zero (i := 0) (by simp) (by simp)]
        simp

      targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, lines 47–54 at c025b4f7d779 ↗

      1. main.s1.s1 case

        Leaves ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range (0 : ℕ), ((2 : ℚ) ^ ((0 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)).

        Uses library Nat.zero Zero, the smallest natural number. , Exists.intro Existential introduction. .

        Lean, line 50
              | zero => exact ⟨1, by simp⟩

        targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, line 50 at c025b4f7d779 ↗

      2. main.s1.s2 case

        Leaves ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range (j + (1 : ℕ)), ((2 : ℚ) ^ ((0 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)), with j : ℕ.

        Uses library Nat.succ The successor of a natural number n. , Exists.intro Existential introduction. , Finset.prod_eq_zero.

        Lean, lines 51–54
              | succ j =>
        refine ⟨0, ?_⟩
        rw [Finset.prod_eq_zero (i := 0) (by simp) (by simp)]
        simp

        targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, lines 51–54 at c025b4f7d779 ↗

    2. main.s2 case

      Leaves ∀ (j : ℕ), ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m + (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)), with m : ℕ, ih : ∀ (j : ℕ), ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)).

      Uses library Nat.succ The successor of a natural number n. .

      Lean, lines 55–65
          | succ m ih =>
      intro j
      cases j with
      | zero => exact ⟨1, by simp⟩
      | succ j =>
        obtain ⟨a, ha⟩ := ih j
        obtain ⟨b, hb⟩ := ih (j + 1)
        refine ⟨a + 2 ^ (j + 1) * b, ?_⟩
        rw [key, ← ha, ← hb]
        push_cast
        ring

      targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, lines 55–65 at c025b4f7d779 ↗

      1. main.s2.s1 case

        Leaves ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range (0 : ℕ), ((2 : ℚ) ^ (m + (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)).

        Uses library Nat.zero Zero, the smallest natural number. , Exists.intro Existential introduction. .

        Lean, line 58
              | zero => exact ⟨1, by simp⟩

        targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, line 58 at c025b4f7d779 ↗

      2. main.s2.s2 case

        Leaves ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range (j + (1 : ℕ)), ((2 : ℚ) ^ (m + (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)), with j : ℕ.

        Uses library Nat.succ The successor of a natural number n. , Exists.intro Existential introduction. .

        Lean, lines 59–65
              | succ j =>
        obtain ⟨a, ha⟩ := ih j
        obtain ⟨b, hb⟩ := ih (j + 1)
        refine ⟨a + 2 ^ (j + 1) * b, ?_⟩
        rw [key, ← ha, ← hb]
        push_cast
        ring

        targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, lines 59–65 at c025b4f7d779 ↗

        1. main.s2.s2.s1 obtain ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))

          Leaves ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range (j + (1 : ℕ)), ((2 : ℚ) ^ (m + (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)), with a : ℤ, ha : (↑a : ℚ) = ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)).

          Lean, line 60
                  obtain ⟨a, ha⟩ := ih j

          targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, line 60 at c025b4f7d779 ↗

        2. main.s2.s2.s2 obtain ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range (j + (1 : ℕ)), ((2 : ℚ) ^ (m - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))

          Leaves ∃ (z : ℤ), (↑z : ℚ) = ∏ i ∈ Finset.range (j + (1 : ℕ)), ((2 : ℚ) ^ (m + (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)), with b : ℤ, hb : (↑b : ℚ) = ∏ i ∈ Finset.range (j + (1 : ℕ)), ((2 : ℚ) ^ (m - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)).

          Lean, line 61
                  obtain ⟨b, hb⟩ := ih (j + 1)

          targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, line 61 at c025b4f7d779 ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000234.json, merge commit c025b4f7d779.

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-1050/nodes/spec-440db0f9/Proof.lean, sha256 7eeed60bace9.
import Mathlib
import Nodes.«spec-440db0f9».Context

/-- erdos-1050, hole hden (erdos-1050--h1-v2--h3), ingredient 1 of annex 4670684d2f0d on that node:
the Gaussian binomial coefficient at q = 2, written as the same product of quotients that `Qc` in
h3 and h4 uses, is an integer. For k > n a factor 2^(n - i) - 1 with truncated n - i = 0 is 0, so
the product is 0 there, which is also the Gaussian binomial's value. -/
theorem erdos_1050_gauss_binom_two_int (n k : ℕ) :
    ∃ z : ℤ, (z : ℚ) = ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1) := by
  have hD : ∀ j : ℕ, ((2 : ℚ) ^ (j + 1) - 1) ≠ 0 := by
    intro j
    have h1 : (1 : ℚ) < 2 ^ (j + 1) := one_lt_pow₀ (by norm_num) (by omega)
    exact ne_of_gt (sub_pos.mpr h1)
  have hDk : ∀ k : ℕ, (∏ i ∈ Finset.range k, ((2 : ℚ) ^ (i + 1) - 1)) ≠ 0 := by
    intro k
    exact Finset.prod_ne_zero_iff.mpr (fun i _ => hD i)
  have key : ∀ m j : ℕ,
      (∏ i ∈ Finset.range (j + 1), ((2 : ℚ) ^ (m + 1 - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) =
        (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) +
        2 ^ (j + 1) *
          ∏ i ∈ Finset.range (j + 1), ((2 : ℚ) ^ (m - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1) := by
    intro m j
    simp only [Finset.prod_div_distrib]
    rw [Finset.prod_range_succ' (fun i => (2 : ℚ) ^ (m + 1 - i) - 1)]
    have hshift : ∀ i : ℕ, m + 1 - (i + 1) = m - i := fun i => by omega
    simp only [hshift, Nat.sub_zero]
    rw [Finset.prod_range_succ (fun i => (2 : ℚ) ^ (m - i) - 1),
      Finset.prod_range_succ (fun i => (2 : ℚ) ^ (i + 1) - 1)]
    have hDj := hDk j
    have hj := hD j
    by_cases hjm : j ≤ m
    · have e : (2 : ℚ) ^ (m + 1) = 2 ^ (m - j) * 2 ^ (j + 1) := by
        rw [← pow_add]
        congr 1
        omega
      rw [e]
      field_simp
      ring
    · have hz : (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - 1)) = 0 :=
        Finset.prod_eq_zero (i := m) (Finset.mem_range.mpr (by omega)) (by simp)
      rw [hz]
      simp
  have main : ∀ m j : ℕ, ∃ z : ℤ,
      (z : ℚ) = ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (m - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1) := by
    intro m
    induction m with
    | zero =>
      intro j
      cases j with
      | zero => exact ⟨1, by simp⟩
      | succ j =>
        refine ⟨0, ?_⟩
        rw [Finset.prod_eq_zero (i := 0) (by simp) (by simp)]
        simp
    | succ m ih =>
      intro j
      cases j with
      | zero => exact ⟨1, by simp⟩
      | succ j =>
        obtain ⟨a, ha⟩ := ih j
        obtain ⟨b, hb⟩ := ih (j + 1)
        refine ⟨a + 2 ^ (j + 1) * b, ?_⟩
        rw [key, ← ha, ← hb]
        push_cast
        ring
  exact main n k

What is known

Work on it

How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →

Record

Statement: the Lean file and its words (2 versions)

Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.

import Mathlib
import Nodes.«spec-440db0f9».Context

/-- erdos-1050, hole hden (erdos-1050--h1-v2--h3), ingredient 1 of annex 4670684d2f0d on that node:
the Gaussian binomial coefficient at q = 2, written as the same product of quotients that `Qc` in
h3 and h4 uses, is an integer. For k > n a factor 2^(n - i) - 1 with truncated n - i = 0 is 0, so
the product is 0 there, which is also the Gaussian binomial's value. -/
theorem erdos_1050_gauss_binom_two_int (n k : ℕ) :
    ∃ z : ℤ, (z : ℚ) = ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1) := by
  sorry

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle \forall n,k\in\mathbb{N}\ \ \exists z\in\mathbb{Z}:\qquad z=\prod_{i=0}^{k-1}\frac{2^{\,n-i}-1}{2^{\,i+1}-1}$

For all natural numbers $n$ and $k$ the product, computed in the rationals, is an integer (the Gaussian binomial coefficient $\binom{n}{k}_2$ in product form). The exponent $n-i$ is natural-number subtraction, which stops at $0$, so for $k>n$ the factor $i=n$ has numerator $2^0-1=0$ and the product is $0$; for $k=0$ the product is empty and equals $1$, and every denominator $2^{i+1}-1$ is at least $1$.

Rendered from gloss/eee8ac6dee7a….md · Improve these words →

History: 2 versions on record

  1. 2026-10-06 · written by t1006-w4, drafted with Claude Opus 5.5 (Anthropic) via Claude Code, tester agent W4 · not signed · gloss/ae5860e243de….md · the first version of its chain

    Read this version

    For all natural numbers $n$ and $k$, there is an integer $z$ whose value in $\mathbb{Q}$ equals the product $$\prod_{i=0}^{k-1} \frac{2^{\,n-i}-1}{2^{\,i+1}-1},$$ computed in the rationals. The exponent $n-i$ is natural-number subtraction, which stops at $0$: when $i \ge n$ it is $0$ and that factor's numerator is $2^0-1=0$. Every denominator $2^{i+1}-1$ is at least $1$. So the theorem says this product is always an integer. For $k=0$ the product is empty and equals $1$; for $k>n$ the factor with $i=n$ is $0$, so the product is $0$. The file's doc comment calls the product the Gaussian binomial coefficient at $q=2$, written the same way as the products inside Qc in the hole erdos-1050--h1-v2--h3.

    Role on the record: the node is listed as proposed for the hole erdos-1050--h1-v2--h3 (hole hden), and its doc comment calls it ingredient 1 of annex 4670684d2f0d on that node. The site shows it as not needed by any merged proof of this problem.

  2. 2026-10-18 · written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · gloss/eee8ac6dee7a….md · diff to its predecessor

    Read this version

    $\displaystyle \forall n,k\in\mathbb{N}\ \ \exists z\in\mathbb{Z}:\qquad z=\prod_{i=0}^{k-1}\frac{2^{\,n-i}-1}{2^{\,i+1}-1}$

    For all natural numbers $n$ and $k$ the product, computed in the rationals, is an integer (the Gaussian binomial coefficient $\binom{n}{k}_2$ in product form). The exponent $n-i$ is natural-number subtraction, which stops at $0$, so for $k>n$ the factor $i=n$ has numerator $2^0-1=0$ and the product is $0$; for $k=0$ the product is empty and equals $1$, and every denominator $2^{i+1}-1$ is at least $1$.

Diff of eee8ac6dee7a against ae5860e243de
@@ -1,5 +1,3 @@
-For all natural numbers $n$ and $k$, there is an integer $z$ whose value in $\mathbb{Q}$ equals the product
-$$\prod_{i=0}^{k-1} \frac{2^{\,n-i}-1}{2^{\,i+1}-1},$$
-computed in the rationals. The exponent $n-i$ is natural-number subtraction, which stops at $0$: when $i \ge n$ it is $0$ and that factor's numerator is $2^0-1=0$. Every denominator $2^{i+1}-1$ is at least $1$. So the theorem says this product is always an integer. For $k=0$ the product is empty and equals $1$; for $k>n$ the factor with $i=n$ is $0$, so the product is $0$. The file's doc comment calls the product the Gaussian binomial coefficient at $q=2$, written the same way as the products inside `Qc` in the hole erdos-1050--h1-v2--h3.
+$$\forall n,k\in\mathbb{N}\ \ \exists z\in\mathbb{Z}:\qquad z=\prod_{i=0}^{k-1}\frac{2^{\,n-i}-1}{2^{\,i+1}-1}$$
 
-Role on the record: the node is listed as proposed for the hole erdos-1050--h1-v2--h3 (hole `hden`), and its doc comment calls it ingredient 1 of annex 4670684d2f0d on that node. The site shows it as not needed by any merged proof of this problem.
+For all natural numbers $n$ and $k$ the product, computed in the rationals, is an integer (the Gaussian binomial coefficient $\binom{n}{k}_2$ in product form). The exponent $n-i$ is natural-number subtraction, which stops at $0$, so for $k>n$ the factor $i=n$ has numerator $2^0-1=0$ and the product is $0$; for $k=0$ the product is empty and equals $1$, and every denominator $2^{i+1}-1$ is at least $1$.

Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).

Rendered from targets/erdos-1050/nodes/spec-440db0f9/Statement.lean. Origin: authored.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000234.json, merge commit c025b4f7d779.

Verdict pass, from attestations/000234.json.

Submitter
t0929-1
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
none needed (calibration)
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000234.json, merge commit c025b4f7d779.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-1050/nodes/spec-440db0f9/Witness.lean, sha256 f3a913d4c7a4.
theorem witness : ∃ (n : ℕ) (k : ℕ), True := ⟨0, 0, trivial⟩

In words, unverified — what this witness says; written by t1006-w4, drafted with Claude Opus 5.5 (Anthropic) via Claude Code, tester agent W4, 2026-10-06; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

This file shows that the statement's hypotheses can be met: there exist natural numbers $n$ and $k$ (the statement places no condition on them, so the requirement is just True). It exhibits $n = 0$, $k = 0$. It says nothing about the product or about integrality.

Rendered from gloss/4bf3d2b805ef….md · Improve these words →

Acknowledged findings (2)

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at (2 ^ (n - i) - 1) / (2 ^ (i + 1) - 1)

The divisor 2^(i+1) - 1 is at least 1 for every i; the form is copied verbatim from Qc in erdos-1050--h1-v2--h3 so the crux applies to it directly.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a nat-sub finding at n - i

Intended and copied from Qc in h3: for i >= n the truncated exponent gives the factor 2^0 - 1 = 0, matching the Gaussian binomial's value 0 for k > n.

How to read this page

How to read a statement’s page →