Open Proof Network

Problems / erdos-1050 / spec-1a5ab7c3

Upper-half Mersenne product clears the denominators

spec-1a5ab7c3 erdos_1050_upper_half_mersenne_clears

proved

Proposed by a contributor.

$\displaystyle \forall n,k\in\mathbb{N},\ k\le n,\ \ \forall c:\mathbb{N}\to\mathbb{Z}\ \ \exists z\in\mathbb{Z}:\qquad z=\Bigl(\prod_{\lfloor n/2\rfloor<m\le n}(2^m-1)\Bigr)\cdot\sum_{j=0}^{k}\frac{c_j}{2^{\,k-j}-1}$

For natural numbers $k\le n$ and any sequence of integers $c_0,c_1,\dots$, the product of $M_n=\prod_{\lfloor n/2\rfloor<m\le n}(2^m-1)$ with the sum is an integer, the arithmetic being in $\mathbb{Q}$ (the integer $z$ is compared with it after coercion). Here $\lfloor n/2\rfloor$ is natural-number division (Lean's n / 2, the product running over Finset.Ioc (n / 2) n), $k-j$ is an ordinary difference since $j\le k$, and the term $j=k$ divides by $2^0-1=0$, which is $0$ in Lean, so in effect the sum runs over $0\le j<k$ with denominators $2^{k-j}-1$, $1\le k-j\le n$.

unverified · history

Lean
theorem erdos_1050_upper_half_mersenne_clears (n k : ℕ) (hk : k ≤ n) (c : ℕ → ℤ) :
    ∃ z : ℤ, (z : ℚ) = (∏ m ∈ Finset.Ioc (n / 2) n, ((2 : ℚ) ^ m - 1)) *
      ∑ j ∈ Finset.range (k + 1), (c j : ℚ) / ((2 : ℚ) ^ (k - j) - 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/137ed18d70be….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

Let $M = \prod_{\lfloor n/2\rfloor < i \le n}(2^i-1)$. The proof names the integer explicitly (lines 33–34): $z = \sum_{j=0}^{k} c_j \cdot \bigl(M \mathbin{/} (2^{k-j}-1)\bigr)$, where $M$ is computed in $\mathbb{Z}$ and $/$ is integer division. It then shows, term by term, that the $j$-th term of $z$ cast to $\mathbb{Q}$ equals $M \cdot c_j/(2^{k-j}-1)$ in $\mathbb{Q}$. The work is the divisibility fact key.

Read it step by step (3 more sections)

Every 2^m - 1 with 1 ≤ m ≤ n divides M

Draft · drafted, by the model named above

key: for $1 \le m \le n$, $(2^m-1) \mid M$ in $\mathbb{Z}$. Put $t = \lfloor n/m \rfloor$. Then $t \ge 1$ (key.ht1), $mt \le n$ (key.hle) and $n < mt + m$ (key.hlt, from $n < m(t+1)$, key.hlt.this). So $mt$ lies in $(\lfloor n/2\rfloor, n]$ (key.hmem): the lower bound because $m \le mt$ (key.hmem.s1.this) together with $n < mt+m$ gives $n < 2mt$ (key.hmem.s1), the upper bound is key.hle (key.hmem.s2). Next, $2^m - 1$ divides $2^{mt}-1$ (key.h1), from $x-1 \mid x^t-1$ with $x = 2^m$ (key.h1.this, Mathlib's sub_dvd_pow_sub_pow). Since $mt$ is one of the indices of $M$, $2^{mt}-1$ is a factor of $M$, and divisibility follows.

The term j = k

Draft · drafted, by the model named above

When $k - j = 0$, the rational term divides by $2^0 - 1 = 0$ and is $0$; the integer term divides by $0$ in $\mathbb{Z}$, also $0$. simp closes it.

The terms j < k

Draft · drafted, by the model named above

Here $1 \le k-j \le k \le n$, so key gives $q$ with $M = (2^{k-j}-1)\,q$ in $\mathbb{Z}$ (s3.s1). The divisor is nonzero in $\mathbb{Z}$ (s3.hne) and in $\mathbb{Q}$ (s3.hneq), since $2^{k-j} \ge 2$. Casting the factorisation to $\mathbb{Q}$ gives $M = (2^{k-j}-1)q$ there too (s3.hP, via s3.hP.this). So the integer division is exact, the $j$-th integer term is $c_j q$, and field_simp checks $c_j q = M c_j/(2^{k-j}-1)$.

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/137ed18d70be….md · the first version of its chain

    Read this version

    Overview

    Let $M = \prod_{\lfloor n/2\rfloor < i \le n}(2^i-1)$. The proof names the integer explicitly (lines 33–34): $z = \sum_{j=0}^{k} c_j \cdot \bigl(M \mathbin{/} (2^{k-j}-1)\bigr)$, where $M$ is computed in $\mathbb{Z}$ and $/$ is integer division. It then shows, term by term, that the $j$-th term of $z$ cast to $\mathbb{Q}$ equals $M \cdot c_j/(2^{k-j}-1)$ in $\mathbb{Q}$. The work is the divisibility fact key.

    Every 2^m - 1 with 1 ≤ m ≤ n divides M (key key.ht1 key.hle key.hlt key.hlt.this key.hmem key.hmem.s1 key.hmem.s1.this key.hmem.s2 key.h1 key.h1.this)

    key: for $1 \le m \le n$, $(2^m-1) \mid M$ in $\mathbb{Z}$. Put $t = \lfloor n/m \rfloor$. Then $t \ge 1$ (key.ht1), $mt \le n$ (key.hle) and $n < mt + m$ (key.hlt, from $n < m(t+1)$, key.hlt.this). So $mt$ lies in $(\lfloor n/2\rfloor, n]$ (key.hmem): the lower bound because $m \le mt$ (key.hmem.s1.this) together with $n < mt+m$ gives $n < 2mt$ (key.hmem.s1), the upper bound is key.hle (key.hmem.s2). Next, $2^m - 1$ divides $2^{mt}-1$ (key.h1), from $x-1 \mid x^t-1$ with $x = 2^m$ (key.h1.this, Mathlib's sub_dvd_pow_sub_pow). Since $mt$ is one of the indices of $M$, $2^{mt}-1$ is a factor of $M$, and divisibility follows.

    The term j = k (s2)

    When $k - j = 0$, the rational term divides by $2^0 - 1 = 0$ and is $0$; the integer term divides by $0$ in $\mathbb{Z}$, also $0$. simp closes it.

    The terms j < k (s3 s3.s1 s3.hne s3.hneq s3.hP s3.hP.this)

    Here $1 \le k-j \le k \le n$, so key gives $q$ with $M = (2^{k-j}-1)\,q$ in $\mathbb{Z}$ (s3.s1). The divisor is nonzero in $\mathbb{Z}$ (s3.hne) and in $\mathbb{Q}$ (s3.hneq), since $2^{k-j} \ge 2$. Casting the factorisation to $\mathbb{Q}$ gives $M = (2^{k-j}-1)q$ there too (s3.hP, via s3.hP.this). So the integer division is exact, the $j$-th integer term is $c_j q$, and field_simp checks $c_j q = M c_j/(2^{k-j}-1)$.

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, 000282, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000282.json, merge commit 23ebf32068e0.

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. key have ∀ (m : ℕ), (1 : ℕ) ≤ m → m ≤ n → (2 : ℤ) ^ m - (1 : ℤ) ∣ ∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℤ) ^ i - (1 : ℤ))

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

    Uses library Finset.Ioc The finset $(a, b]$ of elements x such that a < x and x ≤ b. , Finset.dvd_prod_of_mem.

    Lean, lines 14–32
      have key : ∀ m : ℕ, 1 ≤ m → m ≤ n →
      ((2 : ℤ) ^ m - 1) ∣ ∏ i ∈ Finset.Ioc (n / 2) n, ((2 : ℤ) ^ i - 1) := by
    intro m hm1 hmn
    have ht1 : 1 ≤ n / m := (Nat.one_le_div_iff (by omega)).2 hmn
    have hle : m * (n / m) ≤ n := Nat.mul_div_le n m
    have hlt : n < m * (n / m) + m := by
      have := Nat.lt_mul_div_succ n (show 0 < m by omega)
      rw [Nat.mul_succ] at this
      exact this
    have hmem : m * (n / m) ∈ Finset.Ioc (n / 2) n := by
      rw [Finset.mem_Ioc]
      constructor
      · have : m ≤ m * (n / m) := Nat.le_mul_of_pos_right m (by omega)
        omega
      · exact hle
    have h1 : ((2 : ℤ) ^ m - 1) ∣ (2 : ℤ) ^ (m * (n / m)) - 1 := by
      have := sub_dvd_pow_sub_pow ((2 : ℤ) ^ m) 1 (n / m)
      rwa [one_pow, ← pow_mul] at this
    exact h1.trans (Finset.dvd_prod_of_mem _ hmem)

    targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, lines 14–32 at 23ebf32068e0 ↗

    1. key.ht1 have (1 : ℕ) ≤ n / m

      Leaves (2 : ℤ) ^ m - (1 : ℤ) ∣ ∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℤ) ^ i - (1 : ℤ)), with ht1 : (1 : ℕ) ≤ n / m.

      Uses library Nat.one_le_div_iff.

      Lean, line 17
          have ht1 : 1 ≤ n / m := (Nat.one_le_div_iff (by omega)).2 hmn

      targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, line 17 at 23ebf32068e0 ↗

    2. key.hle have m * (n / m) ≤ n

      Leaves (2 : ℤ) ^ m - (1 : ℤ) ∣ ∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℤ) ^ i - (1 : ℤ)), with hle : m * (n / m) ≤ n.

      Uses library Nat.mul_div_le.

      Lean, line 18
          have hle : m * (n / m) ≤ n := Nat.mul_div_le n m

      targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, line 18 at 23ebf32068e0 ↗

    3. key.hlt have n < m * (n / m) + m

      Leaves (2 : ℤ) ^ m - (1 : ℤ) ∣ ∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℤ) ^ i - (1 : ℤ)), with hlt : n < m * (n / m) + m.

      Uses library Nat.mul_succ.

      Lean, lines 19–22
          have hlt : n < m * (n / m) + m := by
      have := Nat.lt_mul_div_succ n (show 0 < m by omega)
      rw [Nat.mul_succ] at this
      exact this

      targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, lines 19–22 at 23ebf32068e0 ↗

      1. key.hlt.this have n < m * (n / m + (1 : ℕ))

        Leaves n < m * (n / m) + m, with this : n < m * (n / m + (1 : ℕ)).

        Uses library Nat.lt_mul_div_succ.

        Lean, line 20
              have := Nat.lt_mul_div_succ n (show 0 < m by omega)

        targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, line 20 at 23ebf32068e0 ↗

    4. key.hmem have m * (n / m) ∈ Finset.Ioc (n / (2 : ℕ)) n

      Leaves (2 : ℤ) ^ m - (1 : ℤ) ∣ ∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℤ) ^ i - (1 : ℤ)), with hmem : m * (n / m) ∈ Finset.Ioc (n / (2 : ℕ)) n.

      Uses library Finset.Ioc The finset $(a, b]$ of elements x such that a < x and x ≤ b. , Finset.mem_Ioc.

      Lean, lines 23–28
          have hmem : m * (n / m) ∈ Finset.Ioc (n / 2) n := by
      rw [Finset.mem_Ioc]
      constructor
      · have : m ≤ m * (n / m) := Nat.le_mul_of_pos_right m (by omega)
        omega
      · exact hle

      targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, lines 23–28 at 23ebf32068e0 ↗

      1. key.hmem.s1 case

        Leaves n / (2 : ℕ) < m * (n / m).

        Lean, lines 26–27
              · have : m ≤ m * (n / m) := Nat.le_mul_of_pos_right m (by omega)
        omega

        targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, lines 26–27 at 23ebf32068e0 ↗

        1. key.hmem.s1.this have m ≤ m * (n / m)

          Leaves n / (2 : ℕ) < m * (n / m), with this : m ≤ m * (n / m).

          Uses library Nat.le_mul_of_pos_right.

          Lean, line 26
                · have : m ≤ m * (n / m) := Nat.le_mul_of_pos_right m (by omega)

          targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, line 26 at 23ebf32068e0 ↗

      2. key.hmem.s2 case

        Leaves m * (n / m) ≤ n.

        Lean, line 28
              · exact hle

        targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, line 28 at 23ebf32068e0 ↗

    5. key.h1 have (2 : ℤ) ^ m - (1 : ℤ) ∣ (2 : ℤ) ^ (m * (n / m)) - (1 : ℤ)

      Leaves (2 : ℤ) ^ m - (1 : ℤ) ∣ ∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℤ) ^ i - (1 : ℤ)), with h1 : (2 : ℤ) ^ m - (1 : ℤ) ∣ (2 : ℤ) ^ (m * (n / m)) - (1 : ℤ).

      Uses library one_pow, pow_mul.

      Lean, lines 29–31
          have h1 : ((2 : ℤ) ^ m - 1) ∣ (2 : ℤ) ^ (m * (n / m)) - 1 := by
      have := sub_dvd_pow_sub_pow ((2 : ℤ) ^ m) 1 (n / m)
      rwa [one_pow, ← pow_mul] at this

      targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, lines 29–31 at 23ebf32068e0 ↗

      1. key.h1.this have (2 : ℤ) ^ m - (1 : ℤ) ∣ ((2 : ℤ) ^ m) ^ (n / m) - (1 : ℤ) ^ (n / m)

        Leaves (2 : ℤ) ^ m - (1 : ℤ) ∣ (2 : ℤ) ^ (m * (n / m)) - (1 : ℤ), with this : (2 : ℤ) ^ m - (1 : ℤ) ∣ ((2 : ℤ) ^ m) ^ (n / m) - (1 : ℤ) ^ (n / m).

        Uses library sub_dvd_pow_sub_pow.

        Lean, line 30
              have := sub_dvd_pow_sub_pow ((2 : ℤ) ^ m) 1 (n / m)

        targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, line 30 at 23ebf32068e0 ↗

  2. s2 case routine: simp

    Leaves (↑(c j * ((∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℤ) ^ i - (1 : ℤ))) / ((2 : ℤ) ^ (k - j) - (1 : ℤ)))) : ℚ) = (∏ m ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℚ) ^ m - (1 : ℚ))) * ((↑(c j) : ℚ) / ((2 : ℚ) ^ (k - j) - (1 : ℚ))).

    Lean, line 40
      · simp [h0]

    targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, line 40 at 23ebf32068e0 ↗

  3. s3 case

    Leaves (↑(c j * ((∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℤ) ^ i - (1 : ℤ))) / ((2 : ℤ) ^ (k - j) - (1 : ℤ)))) : ℚ) = (∏ m ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℚ) ^ m - (1 : ℚ))) * ((↑(c j) : ℚ) / ((2 : ℚ) ^ (k - j) - (1 : ℚ))).

    Uses library Int.mul_ediv_cancel_left.

    Lean, lines 41–54
      · obtain ⟨q, hq⟩ := key (k - j) (by omega) (by omega)
    have hne : ((2 : ℤ) ^ (k - j) - 1) ≠ 0 := by
      have : (2 : ℤ) ^ 1 ≤ 2 ^ (k - j) := pow_le_pow_right₀ (by norm_num) (by omega)
      linarith
    have hneq : ((2 : ℚ) ^ (k - j) - 1) ≠ 0 := by
      have : (2 : ℚ) ^ 1 ≤ 2 ^ (k - j) := pow_le_pow_right₀ (by norm_num) (by omega)
      linarith
    have hP : (∏ i ∈ Finset.Ioc (n / 2) n, ((2 : ℚ) ^ i - 1)) = ((2 : ℚ) ^ (k - j) - 1) * (q : ℚ) := by
      have := congrArg (fun z : ℤ => (z : ℚ)) hq
      push_cast at this
      exact this
    rw [hq, Int.mul_ediv_cancel_left _ hne, hP]
    push_cast
    field_simp

    targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, lines 41–54 at 23ebf32068e0 ↗

    1. s3.s1 obtain (2 : ℤ) ^ (k - j) - (1 : ℤ) ∣ ∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℤ) ^ i - (1 : ℤ))

      Leaves (↑(c j * ((∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℤ) ^ i - (1 : ℤ))) / ((2 : ℤ) ^ (k - j) - (1 : ℤ)))) : ℚ) = (∏ m ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℚ) ^ m - (1 : ℚ))) * ((↑(c j) : ℚ) / ((2 : ℚ) ^ (k - j) - (1 : ℚ))), with q : ℤ, hq : ∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℤ) ^ i - (1 : ℤ)) = ((2 : ℤ) ^ (k - j) - (1 : ℤ)) * q.

      Lean, line 41
        · obtain ⟨q, hq⟩ := key (k - j) (by omega) (by omega)

      targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, line 41 at 23ebf32068e0 ↗

    2. s3.hne have (2 : ℤ) ^ (k - j) - (1 : ℤ) ≠ (0 : ℤ)

      Leaves (↑(c j * ((∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℤ) ^ i - (1 : ℤ))) / ((2 : ℤ) ^ (k - j) - (1 : ℤ)))) : ℚ) = (∏ m ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℚ) ^ m - (1 : ℚ))) * ((↑(c j) : ℚ) / ((2 : ℚ) ^ (k - j) - (1 : ℚ))), with hne : (2 : ℤ) ^ (k - j) - (1 : ℤ) ≠ (0 : ℤ).

      Lean, lines 42–44
          have hne : ((2 : ℤ) ^ (k - j) - 1) ≠ 0 := by
      have : (2 : ℤ) ^ 1 ≤ 2 ^ (k - j) := pow_le_pow_right₀ (by norm_num) (by omega)
      linarith

      targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, lines 42–44 at 23ebf32068e0 ↗

      1. s3.hne.this have (2 : ℤ) ^ (1 : ℕ) ≤ (2 : ℤ) ^ (k - j)

        Leaves (2 : ℤ) ^ (k - j) - (1 : ℤ) ≠ (0 : ℤ), with this : (2 : ℤ) ^ (1 : ℕ) ≤ (2 : ℤ) ^ (k - j).

        Uses library pow_le_pow_right₀.

        Lean, line 43
              have : (2 : ℤ) ^ 1 ≤ 2 ^ (k - j) := pow_le_pow_right₀ (by norm_num) (by omega)

        targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, line 43 at 23ebf32068e0 ↗

    3. s3.hneq have (2 : ℚ) ^ (k - j) - (1 : ℚ) ≠ (0 : ℚ)

      Leaves (↑(c j * ((∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℤ) ^ i - (1 : ℤ))) / ((2 : ℤ) ^ (k - j) - (1 : ℤ)))) : ℚ) = (∏ m ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℚ) ^ m - (1 : ℚ))) * ((↑(c j) : ℚ) / ((2 : ℚ) ^ (k - j) - (1 : ℚ))), with hneq : (2 : ℚ) ^ (k - j) - (1 : ℚ) ≠ (0 : ℚ).

      Lean, lines 45–47
          have hneq : ((2 : ℚ) ^ (k - j) - 1) ≠ 0 := by
      have : (2 : ℚ) ^ 1 ≤ 2 ^ (k - j) := pow_le_pow_right₀ (by norm_num) (by omega)
      linarith

      targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, lines 45–47 at 23ebf32068e0 ↗

      1. s3.hneq.this have (2 : ℚ) ^ (1 : ℕ) ≤ (2 : ℚ) ^ (k - j)

        Leaves (2 : ℚ) ^ (k - j) - (1 : ℚ) ≠ (0 : ℚ), with this : (2 : ℚ) ^ (1 : ℕ) ≤ (2 : ℚ) ^ (k - j).

        Uses library pow_le_pow_right₀.

        Lean, line 46
              have : (2 : ℚ) ^ 1 ≤ 2 ^ (k - j) := pow_le_pow_right₀ (by norm_num) (by omega)

        targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, line 46 at 23ebf32068e0 ↗

    4. s3.hP have ∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℚ) ^ i - (1 : ℚ)) = ((2 : ℚ) ^ (k - j) - (1 : ℚ)) * (↑q : ℚ)

      Leaves (↑(c j * ((∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℤ) ^ i - (1 : ℤ))) / ((2 : ℤ) ^ (k - j) - (1 : ℤ)))) : ℚ) = (∏ m ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℚ) ^ m - (1 : ℚ))) * ((↑(c j) : ℚ) / ((2 : ℚ) ^ (k - j) - (1 : ℚ))), with hP : ∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℚ) ^ i - (1 : ℚ)) = ((2 : ℚ) ^ (k - j) - (1 : ℚ)) * (↑q : ℚ).

      Uses library Finset.Ioc The finset $(a, b]$ of elements x such that a < x and x ≤ b. .

      Lean, lines 48–51
          have hP : (∏ i ∈ Finset.Ioc (n / 2) n, ((2 : ℚ) ^ i - 1)) = ((2 : ℚ) ^ (k - j) - 1) * (q : ℚ) := by
      have := congrArg (fun z : ℤ => (z : ℚ)) hq
      push_cast at this
      exact this

      targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, lines 48–51 at 23ebf32068e0 ↗

      1. s3.hP.this have (↑(∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℤ) ^ i - (1 : ℤ))) : ℚ) = (↑(((2 : ℤ) ^ (k - j) - (1 : ℤ)) * q) : ℚ)

        Leaves ∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℚ) ^ i - (1 : ℚ)) = ((2 : ℚ) ^ (k - j) - (1 : ℚ)) * (↑q : ℚ), with this : (↑(∏ i ∈ Finset.Ioc (n / (2 : ℕ)) n, ((2 : ℤ) ^ i - (1 : ℤ))) : ℚ) = (↑(((2 : ℤ) ^ (k - j) - (1 : ℤ)) * q) : ℚ).

        Uses library congrArg Congruence in the function argument: if a₁ = a₂ then f a₁ = f a₂ for any (nondependent) function f. .

        Lean, line 49
              have := congrArg (fun z : ℤ => (z : ℚ)) hq

        targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean, line 49 at 23ebf32068e0 ↗

The proof in Lean (Proof.lean)

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

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-1a5ab7c3/Proof.lean, sha256 fb2d53c7f931.
import Mathlib
import Nodes.«spec-1a5ab7c3».Context

/-- erdos-1050, hole hden (erdos-1050--h1-v2--h3), ingredient 2, odd half, of annex 4670684d2f0d
on that node. Every denominator 2^(k - j) - 1 with 1 ≤ k - j ≤ n divides
M_n = ∏_{n/2 < m ≤ n} (2^m - 1), because m has the multiple m * (n / m) in (n/2, n]. Hence M_n
clears the inner sum p_k(n) = ∑_{j ≤ k} Qc n j / (2^(k - j) - 1) of `Aq` in h3 for any integer
coefficients (Qc n j is one by ingredient 1, spec-440db0f9). The j = k term divides by 2^0 - 1 = 0
and is 0 in ℚ, as in h3. The 2-adic half of ingredient 2 (v2(p_k(n)) ≥ k(k-1)/2) is not claimed. -/
theorem erdos_1050_upper_half_mersenne_clears (n k : ℕ) (hk : k ≤ n) (c : ℕ → ℤ) :
    ∃ z : ℤ, (z : ℚ) = (∏ m ∈ Finset.Ioc (n / 2) n, ((2 : ℚ) ^ m - 1)) *
      ∑ j ∈ Finset.range (k + 1), (c j : ℚ) / ((2 : ℚ) ^ (k - j) - 1) := by
  -- every 2^m - 1 with 1 ≤ m ≤ n divides the product over the upper half (n/2, n]
  have key : ∀ m : ℕ, 1 ≤ m → m ≤ n →
      ((2 : ℤ) ^ m - 1) ∣ ∏ i ∈ Finset.Ioc (n / 2) n, ((2 : ℤ) ^ i - 1) := by
    intro m hm1 hmn
    have ht1 : 1 ≤ n / m := (Nat.one_le_div_iff (by omega)).2 hmn
    have hle : m * (n / m) ≤ n := Nat.mul_div_le n m
    have hlt : n < m * (n / m) + m := by
      have := Nat.lt_mul_div_succ n (show 0 < m by omega)
      rw [Nat.mul_succ] at this
      exact this
    have hmem : m * (n / m) ∈ Finset.Ioc (n / 2) n := by
      rw [Finset.mem_Ioc]
      constructor
      · have : m ≤ m * (n / m) := Nat.le_mul_of_pos_right m (by omega)
        omega
      · exact hle
    have h1 : ((2 : ℤ) ^ m - 1) ∣ (2 : ℤ) ^ (m * (n / m)) - 1 := by
      have := sub_dvd_pow_sub_pow ((2 : ℤ) ^ m) 1 (n / m)
      rwa [one_pow, ← pow_mul] at this
    exact h1.trans (Finset.dvd_prod_of_mem _ hmem)
  refine ⟨∑ j ∈ Finset.range (k + 1),
      c j * ((∏ i ∈ Finset.Ioc (n / 2) n, ((2 : ℤ) ^ i - 1)) / ((2 : ℤ) ^ (k - j) - 1)), ?_⟩
  rw [Int.cast_sum, Finset.mul_sum]
  apply Finset.sum_congr rfl
  intro j hj
  rw [Finset.mem_range] at hj
  by_cases h0 : k - j = 0
  · simp [h0]
  · obtain ⟨q, hq⟩ := key (k - j) (by omega) (by omega)
    have hne : ((2 : ℤ) ^ (k - j) - 1) ≠ 0 := by
      have : (2 : ℤ) ^ 1 ≤ 2 ^ (k - j) := pow_le_pow_right₀ (by norm_num) (by omega)
      linarith
    have hneq : ((2 : ℚ) ^ (k - j) - 1) ≠ 0 := by
      have : (2 : ℚ) ^ 1 ≤ 2 ^ (k - j) := pow_le_pow_right₀ (by norm_num) (by omega)
      linarith
    have hP : (∏ i ∈ Finset.Ioc (n / 2) n, ((2 : ℚ) ^ i - 1)) = ((2 : ℚ) ^ (k - j) - 1) * (q : ℚ) := by
      have := congrArg (fun z : ℤ => (z : ℚ)) hq
      push_cast at this
      exact this
    rw [hq, Int.mul_ediv_cancel_left _ hne, hP]
    push_cast
    field_simp

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-1a5ab7c3».Context

/-- erdos-1050, hole hden (erdos-1050--h1-v2--h3), ingredient 2, odd half, of annex 4670684d2f0d
on that node. Every denominator 2^(k - j) - 1 with 1 ≤ k - j ≤ n divides
M_n = ∏_{n/2 < m ≤ n} (2^m - 1), because m has the multiple m * (n / m) in (n/2, n]. Hence M_n
clears the inner sum p_k(n) = ∑_{j ≤ k} Qc n j / (2^(k - j) - 1) of `Aq` in h3 for any integer
coefficients (Qc n j is one by ingredient 1, spec-440db0f9). The j = k term divides by 2^0 - 1 = 0
and is 0 in ℚ, as in h3. The 2-adic half of ingredient 2 (v2(p_k(n)) ≥ k(k-1)/2) is not claimed. -/
theorem erdos_1050_upper_half_mersenne_clears (n k : ℕ) (hk : k ≤ n) (c : ℕ → ℤ) :
    ∃ z : ℤ, (z : ℚ) = (∏ m ∈ Finset.Ioc (n / 2) n, ((2 : ℚ) ^ m - 1)) *
      ∑ j ∈ Finset.range (k + 1), (c j : ℚ) / ((2 : ℚ) ^ (k - j) - 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},\ k\le n,\ \ \forall c:\mathbb{N}\to\mathbb{Z}\ \ \exists z\in\mathbb{Z}:\qquad z=\Bigl(\prod_{\lfloor n/2\rfloor<m\le n}(2^m-1)\Bigr)\cdot\sum_{j=0}^{k}\frac{c_j}{2^{\,k-j}-1}$

For natural numbers $k\le n$ and any sequence of integers $c_0,c_1,\dots$, the product of $M_n=\prod_{\lfloor n/2\rfloor<m\le n}(2^m-1)$ with the sum is an integer, the arithmetic being in $\mathbb{Q}$ (the integer $z$ is compared with it after coercion). Here $\lfloor n/2\rfloor$ is natural-number division (Lean's n / 2, the product running over Finset.Ioc (n / 2) n), $k-j$ is an ordinary difference since $j\le k$, and the term $j=k$ divides by $2^0-1=0$, which is $0$ in Lean, so in effect the sum runs over $0\le j<k$ with denominators $2^{k-j}-1$, $1\le k-j\le n$.

Rendered from gloss/7d0bf503705b….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/4e513a6eb7be….md · the first version of its chain

    Read this version

    For natural numbers $n$ and $k$ with $k \le n$, and any sequence of integers $c_0, c_1, c_2, \dots$ (a function $c : \mathbb{N} \to \mathbb{Z}$), there is an integer $z$ whose value in $\mathbb{Q}$ equals $$\Bigl(\prod_{\lfloor n/2\rfloor < m \le n} (2^m-1)\Bigr)\cdot \sum_{j=0}^{k} \frac{c_j}{2^{\,k-j}-1},$$ computed in the rationals. Here $\lfloor n/2 \rfloor$ is natural-number division (the Lean n / 2), so the product runs over the integers $m$ with $\lfloor n/2\rfloor < m \le n$. Since $j \le k$, $k-j$ is an ordinary difference. The last term, $j=k$, divides by $2^0-1=0$, and in Lean division by zero gives $0$, so that term contributes nothing: in effect the sum is over $0 \le j < k$, with denominators $2^{k-j}-1$ for $1 \le k-j \le k \le n$. In words: multiplying by $M_n = \prod_{\lfloor n/2\rfloor < m \le n}(2^m-1)$ clears every denominator of such a sum, whatever the integer coefficients.

    The doc comment says why the authors expected it (each $d$ with $1 \le d \le n$ has a multiple in $(n/2, n]$, so $2^d-1$ divides some $2^m-1$ in the product) and says that the 2-adic half of its ingredient is not claimed here; the theorem itself makes no 2-adic statement.

    Role on the record: the node is listed as proposed for the hole erdos-1050--h1-v2--h3 (hole hden), where the inner sums of Aq have this shape with $c_j$ the values Qc n j; its doc comment calls it the odd half of ingredient 2 of annex 4670684d2f0d. 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/7d0bf503705b….md · diff to its predecessor

    Read this version

    $\displaystyle \forall n,k\in\mathbb{N},\ k\le n,\ \ \forall c:\mathbb{N}\to\mathbb{Z}\ \ \exists z\in\mathbb{Z}:\qquad z=\Bigl(\prod_{\lfloor n/2\rfloor<m\le n}(2^m-1)\Bigr)\cdot\sum_{j=0}^{k}\frac{c_j}{2^{\,k-j}-1}$

    For natural numbers $k\le n$ and any sequence of integers $c_0,c_1,\dots$, the product of $M_n=\prod_{\lfloor n/2\rfloor<m\le n}(2^m-1)$ with the sum is an integer, the arithmetic being in $\mathbb{Q}$ (the integer $z$ is compared with it after coercion). Here $\lfloor n/2\rfloor$ is natural-number division (Lean's n / 2, the product running over Finset.Ioc (n / 2) n), $k-j$ is an ordinary difference since $j\le k$, and the term $j=k$ divides by $2^0-1=0$, which is $0$ in Lean, so in effect the sum runs over $0\le j<k$ with denominators $2^{k-j}-1$, $1\le k-j\le n$.

Diff of 7d0bf503705b against 4e513a6eb7be
@@ -1,7 +1,3 @@
-For natural numbers $n$ and $k$ with $k \le n$, and any sequence of integers $c_0, c_1, c_2, \dots$ (a function $c : \mathbb{N} \to \mathbb{Z}$), there is an integer $z$ whose value in $\mathbb{Q}$ equals
-$$\Bigl(\prod_{\lfloor n/2\rfloor < m \le n} (2^m-1)\Bigr)\cdot \sum_{j=0}^{k} \frac{c_j}{2^{\,k-j}-1},$$
-computed in the rationals. Here $\lfloor n/2 \rfloor$ is natural-number division (the Lean `n / 2`), so the product runs over the integers $m$ with $\lfloor n/2\rfloor < m \le n$. Since $j \le k$, $k-j$ is an ordinary difference. The last term, $j=k$, divides by $2^0-1=0$, and in Lean division by zero gives $0$, so that term contributes nothing: in effect the sum is over $0 \le j < k$, with denominators $2^{k-j}-1$ for $1 \le k-j \le k \le n$. In words: multiplying by $M_n = \prod_{\lfloor n/2\rfloor < m \le n}(2^m-1)$ clears every denominator of such a sum, whatever the integer coefficients.
+$$\forall n,k\in\mathbb{N},\ k\le n,\ \ \forall c:\mathbb{N}\to\mathbb{Z}\ \ \exists z\in\mathbb{Z}:\qquad z=\Bigl(\prod_{\lfloor n/2\rfloor<m\le n}(2^m-1)\Bigr)\cdot\sum_{j=0}^{k}\frac{c_j}{2^{\,k-j}-1}$$
 
-The doc comment says why the authors expected it (each $d$ with $1 \le d \le n$ has a multiple in $(n/2, n]$, so $2^d-1$ divides some $2^m-1$ in the product) and says that the 2-adic half of its ingredient is not claimed here; the theorem itself makes no 2-adic statement.
-
-Role on the record: the node is listed as proposed for the hole erdos-1050--h1-v2--h3 (hole `hden`), where the inner sums of `Aq` have this shape with $c_j$ the values `Qc n j`; its doc comment calls it the odd half of ingredient 2 of annex 4670684d2f0d. The site shows it as not needed by any merged proof of this problem.
+For natural numbers $k\le n$ and any sequence of integers $c_0,c_1,\dots$, the product of $M_n=\prod_{\lfloor n/2\rfloor<m\le n}(2^m-1)$ with the sum is an integer, the arithmetic being in $\mathbb{Q}$ (the integer $z$ is compared with it after coercion). Here $\lfloor n/2\rfloor$ is natural-number division (Lean's `n / 2`, the product running over `Finset.Ioc (n / 2) n`), $k-j$ is an ordinary difference since $j\le k$, and the term $j=k$ divides by $2^0-1=0$, which is $0$ in Lean, so in effect the sum runs over $0\le j<k$ with denominators $2^{k-j}-1$, $1\le k-j\le n$.

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-1a5ab7c3/Statement.lean. Origin: authored.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000282.json, merge commit 23ebf32068e0.

Verdict pass, from attestations/000282.json.

Submitter
t0929-2
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/000282.json, merge commit 23ebf32068e0.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-1050/nodes/spec-1a5ab7c3/Witness.lean, sha256 ea72d9220e1f.
import Mathlib

theorem witness : ∃ (n : ℕ) (k : ℕ) (c : ℕ → ℤ), k ≤ n := ⟨0, 0, fun _ => 0, le_refl 0⟩

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 together: there exist natural numbers $n$, $k$ and a function $c : \mathbb{N}\to\mathbb{Z}$ with $k \le n$. It exhibits $n = 0$, $k = 0$ and the constant function $c = 0$. It says nothing about the product or the sum.

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

Acknowledged findings (3)

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

Untrusted: acknowledgment of a div-zero finding at ↑(c j) / (2 ^ (k - j) - 1)

Intended and matches h3: the divisor is 0 exactly at j = k, where Lean's x / 0 = 0 makes that term 0, as in the inner sum of Aq in erdos-1050--h1-v2--h3.

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

Untrusted: acknowledgment of a nat-sub finding at k - j

j ranges over range (k + 1), so j ≤ k and k - j never truncates; the same expression appears in h3's Aq.

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

Untrusted: acknowledgment of a off-by-one-range finding at Finset.range (k + 1)

The sum is over 0 ≤ j ≤ k inclusive, exactly the inner sum p_k(n) of Aq in h3.

How to read this page

How to read a statement’s page →