Open Proof Network

Problems / erdos-69 / spec-7f0efe19

Prescribed lower bounds for omega on a window

spec-7f0efe19 Opn.erdos_69_omega_window

proved

Proposed by a contributor.

$\displaystyle \forall k\in\mathbb{N},\ \forall c:\mathbb{N}\to\mathbb{N}\ \ \exists N\in\mathbb{N}\ \ \forall j<k:\quad c(j) \le \omega(N+1+j)$

For every length k and every sequence of naturals c there is a natural N with c(j) ≤ ω(N+1+j) for each j < k, where ω(n) is the number of distinct prime factors of n.

unverified · history

Lean
theorem Opn.erdos_69_omega_window :
    ∀ (k : ℕ) (c : ℕ → ℕ), ∃ N : ℕ, ∀ j < k, c j ≤ ω (N + 1 + j) := 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 →

How it was proved

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

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000301.json, merge commit 0b4c88bbdf03.

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. hqp have ∀ (x : ℕ × ℕ), Nat.Prime (q x)

    Leaves ∃ (N : ℕ), ∀ j < k, c j ≤ (ω : ℕ → ℕ) (N + (1 : ℕ) + j), with hqp : ∀ (x : ℕ × ℕ), Nat.Prime (q x).

    Uses library Nat.prime_nth_prime.

    Lean, line 20
      have hqp : ∀ x, (q x).Prime := fun x => Nat.prime_nth_prime _

    targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, line 20 at 0b4c88bbdf03 ↗

  2. hqinj have Function.Injective q

    Leaves ∃ (N : ℕ), ∀ j < k, c j ≤ (ω : ℕ → ℕ) (N + (1 : ℕ) + j), with hqinj : Function.Injective q.

    Uses library Function.Injective A function f : α → β is called injective if f x = f y implies x = y. , Prod.ext.

    Lean, lines 21–26
      have hqinj : Function.Injective q := by
    intro x y h
    have h1 : Nat.pair x.1 x.2 = Nat.pair y.1 y.2 :=
      Nat.nth_injective Nat.infinite_setOfPred_prime h
    obtain ⟨h2, h3⟩ := Nat.pair_eq_pair.1 h1
    exact Prod.ext h2 h3

    targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, lines 21–26 at 0b4c88bbdf03 ↗

    1. hqinj.h1 have Nat.pair x.1 x.2 = Nat.pair y.1 y.2

      Leaves x = y, with h1 : Nat.pair x.1 x.2 = Nat.pair y.1 y.2.

      Uses library Nat.pair Pairing function for the natural numbers. , Nat.nth_injective, Nat.infinite_setOfPred_prime A version of Nat.exists_infinite_primes using the Set.Infinite predicate. .

      Lean, lines 23–24
          have h1 : Nat.pair x.1 x.2 = Nat.pair y.1 y.2 :=
      Nat.nth_injective Nat.infinite_setOfPred_prime h

      targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, lines 23–24 at 0b4c88bbdf03 ↗

    2. hqinj.s2 obtain x.1 = y.1 ∧ x.2 = y.2

      Leaves x = y, with h2 : x.1 = y.1, h3 : x.2 = y.2.

      Uses library Nat.pair_eq_pair.

      Lean, line 25
          obtain ⟨h2, h3⟩ := Nat.pair_eq_pair.1 h1

      targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, line 25 at 0b4c88bbdf03 ↗

  3. hmem have ∀ (j i : ℕ), j < k → i < c j → (j, i) ∈ t

    Leaves ∃ (N : ℕ), ∀ j < k, c j ≤ (ω : ℕ → ℕ) (N + (1 : ℕ) + j), with hmem : ∀ (j i : ℕ), j < k → i < c j → (j, i) ∈ t.

    Uses library Finset.mem_filter, Finset.mem_product, Finset.mem_range, And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. , lt_of_lt_of_le, Finset.le_sup.

    Lean, lines 29–33
      have hmem : ∀ j i, j < k → i < c j → (j, i) ∈ t := by
    intro j i hj hi
    simp only [t, Finset.mem_filter, Finset.mem_product, Finset.mem_range]
    refine ⟨⟨hj, lt_of_lt_of_le hi ?_⟩, hi⟩
    exact Finset.le_sup (f := c) (Finset.mem_range.2 hj)

    targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, lines 29–33 at 0b4c88bbdf03 ↗

  4. ht have ∀ x ∈ t, x.1 < k

    Leaves ∃ (N : ℕ), ∀ j < k, c j ≤ (ω : ℕ → ℕ) (N + (1 : ℕ) + j), with ht : ∀ x ∈ t, x.1 < k.

    Uses library Finset.mem_filter, Finset.mem_product, Finset.mem_range.

    Lean, lines 34–37
      have ht : ∀ x ∈ t, x.1 < k := by
    intro x hx
    simp only [t, Finset.mem_filter, Finset.mem_product, Finset.mem_range] at hx
    exact hx.1.1

    targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, lines 34–37 at 0b4c88bbdf03 ↗

  5. hq0 have ∀ x ∈ t, q x ≠ (0 : ℕ)

    Leaves ∃ (N : ℕ), ∀ j < k, c j ≤ (ω : ℕ → ℕ) (N + (1 : ℕ) + j), with hq0 : ∀ x ∈ t, q x ≠ (0 : ℕ).

    Lean, line 38
      have hq0 : ∀ x ∈ t, q x ≠ 0 := fun x _ => (hqp x).ne_zero

    targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, line 38 at 0b4c88bbdf03 ↗

  6. hcop have (↑t : Set (ℕ × ℕ)).Pairwise (Function.onFun Nat.Coprime q)

    Leaves ∃ (N : ℕ), ∀ j < k, c j ≤ (ω : ℕ → ℕ) (N + (1 : ℕ) + j), with hcop : (↑t : Set (ℕ × ℕ)).Pairwise (Function.onFun Nat.Coprime q).

    Uses library Set A set is a collection of elements of some type α. , Function.onFun Given functions f : β → β → φ and g : α → β, produce a function α → α → φ that evaluates g on each argument, then applies f to the results. , Nat.Coprime m and n are coprime, or relatively prime, if their gcd is 1. , Nat.coprime_primes.

    Lean, lines 39–41
      have hcop : (↑t : Set (ℕ × ℕ)).Pairwise (Function.onFun Nat.Coprime q) := by
    intro x _ y _ hxy
    exact (Nat.coprime_primes (hqp x) (hqp y)).2 (hqinj.ne hxy)

    targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, lines 39–41 at 0b4c88bbdf03 ↗

  7. s7 obtain { k : ℕ // ∀ i ∈ t, k ≡ a i [MOD q i] }

    Leaves ∃ (N : ℕ), ∀ j < k, c j ≤ (ω : ℕ → ℕ) (N + (1 : ℕ) + j), with N : ℕ, hN : ∀ i ∈ t, N ≡ a i [MOD q i].

    Uses library Nat.chineseRemainderOfFinset The natural number less than ∏ i ∈ t, s i congruent to a i mod s i for all i ∈ t. .

    Lean, line 43
      obtain ⟨N, hN⟩ := Nat.chineseRemainderOfFinset a q t hq0 hcop

    targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, line 43 at 0b4c88bbdf03 ↗

  8. hdvd have ∀ i < c j, q (j, i) ∣ N + (1 : ℕ) + j

    Leaves c j ≤ (ω : ℕ → ℕ) (N + (1 : ℕ) + j), with hdvd : ∀ i < c j, q (j, i) ∣ N + (1 : ℕ) + j.

    Uses library add_assoc.

    Lean, lines 45–58
      have hdvd : ∀ i < c j, q (j, i) ∣ N + 1 + j := by
    intro i hi
    have hx := hmem j i hj hi
    have h1 : N ≡ a (j, i) [MOD q (j, i)] := hN _ hx
    have h2 : 1 + j ≤ (k + 1) * q (j, i) := by
      have : 2 ≤ q (j, i) := (hqp _).two_le
      nlinarith
    have h3 : N + (1 + j) ≡ (k + 1) * q (j, i) [MOD q (j, i)] := by
      have := h1.add_right (1 + j)
      simpa [a, Nat.sub_add_cancel h2] using this
    have h4 : (k + 1) * q (j, i) ≡ 0 [MOD q (j, i)] :=
      (Nat.modEq_zero_iff_dvd).2 (dvd_mul_left _ _)
    have h5 := (Nat.modEq_zero_iff_dvd).1 (h3.trans h4)
    simpa [add_assoc] using h5

    targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, lines 45–58 at 0b4c88bbdf03 ↗

    1. hdvd.hx have (j, i) ∈ t

      Leaves q (j, i) ∣ N + (1 : ℕ) + j, with hx : (j, i) ∈ t.

      Lean, line 47
          have hx := hmem j i hj hi

      targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, line 47 at 0b4c88bbdf03 ↗

    2. hdvd.h1 have N ≡ a (j, i) [MOD q (j, i)]

      Leaves q (j, i) ∣ N + (1 : ℕ) + j, with h1 : N ≡ a (j, i) [MOD q (j, i)].

      Lean, line 48
          have h1 : N ≡ a (j, i) [MOD q (j, i)] := hN _ hx

      targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, line 48 at 0b4c88bbdf03 ↗

    3. hdvd.h2 have (1 : ℕ) + j ≤ (k + (1 : ℕ)) * q (j, i)

      Leaves q (j, i) ∣ N + (1 : ℕ) + j, with h2 : (1 : ℕ) + j ≤ (k + (1 : ℕ)) * q (j, i).

      Lean, lines 49–51
          have h2 : 1 + j ≤ (k + 1) * q (j, i) := by
      have : 2 ≤ q (j, i) := (hqp _).two_le
      nlinarith

      targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, lines 49–51 at 0b4c88bbdf03 ↗

      1. hdvd.h2.this have (2 : ℕ) ≤ q (j, i)

        Leaves (1 : ℕ) + j ≤ (k + (1 : ℕ)) * q (j, i), with this : (2 : ℕ) ≤ q (j, i).

        Lean, line 50
              have : 2 ≤ q (j, i) := (hqp _).two_le

        targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, line 50 at 0b4c88bbdf03 ↗

    4. hdvd.h3 have N + ((1 : ℕ) + j) ≡ (k + (1 : ℕ)) * q (j, i) [MOD q (j, i)]

      Leaves q (j, i) ∣ N + (1 : ℕ) + j, with h3 : N + ((1 : ℕ) + j) ≡ (k + (1 : ℕ)) * q (j, i) [MOD q (j, i)].

      Uses library Nat.sub_add_cancel.

      Lean, lines 52–54
          have h3 : N + (1 + j) ≡ (k + 1) * q (j, i) [MOD q (j, i)] := by
      have := h1.add_right (1 + j)
      simpa [a, Nat.sub_add_cancel h2] using this

      targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, lines 52–54 at 0b4c88bbdf03 ↗

      1. hdvd.h3.this have N + ((1 : ℕ) + j) ≡ a (j, i) + ((1 : ℕ) + j) [MOD q (j, i)]

        Leaves N + ((1 : ℕ) + j) ≡ (k + (1 : ℕ)) * q (j, i) [MOD q (j, i)], with this : N + ((1 : ℕ) + j) ≡ a (j, i) + ((1 : ℕ) + j) [MOD q (j, i)].

        Lean, line 53
              have := h1.add_right (1 + j)

        targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, line 53 at 0b4c88bbdf03 ↗

    5. hdvd.h4 have (k + (1 : ℕ)) * q (j, i) ≡ (0 : ℕ) [MOD q (j, i)]

      Leaves q (j, i) ∣ N + (1 : ℕ) + j, with h4 : (k + (1 : ℕ)) * q (j, i) ≡ (0 : ℕ) [MOD q (j, i)].

      Uses library Nat.modEq_zero_iff_dvd, dvd_mul_left.

      Lean, lines 55–56
          have h4 : (k + 1) * q (j, i) ≡ 0 [MOD q (j, i)] :=
      (Nat.modEq_zero_iff_dvd).2 (dvd_mul_left _ _)

      targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, lines 55–56 at 0b4c88bbdf03 ↗

    6. hdvd.h5 have q (j, i) ∣ N + ((1 : ℕ) + j)

      Leaves q (j, i) ∣ N + (1 : ℕ) + j, with h5 : q (j, i) ∣ N + ((1 : ℕ) + j).

      Uses library Nat.modEq_zero_iff_dvd.

      Lean, line 57
          have h5 := (Nat.modEq_zero_iff_dvd).1 (h3.trans h4)

      targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, line 57 at 0b4c88bbdf03 ↗

  9. h_x3c9 (hω) have (ω : ℕ → ℕ) (N + (1 : ℕ) + j) = (N + (1 : ℕ) + j).primeFactors.card

    Leaves c j ≤ (ω : ℕ → ℕ) (N + (1 : ℕ) + j), with hω : (ω : ℕ → ℕ) (N + (1 : ℕ) + j) = (N + (1 : ℕ) + j).primeFactors.card.

    Uses library ArithmeticFunction.cardDistinctFactors_apply, Nat.primeFactors The prime factors of a natural number as a finset. , List.card_toFinset.

    Lean, lines 59–60
      have hω : ω (N + 1 + j) = (N + 1 + j).primeFactors.card := by
    rw [ArithmeticFunction.cardDistinctFactors_apply, Nat.primeFactors, List.card_toFinset]

    targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, lines 59–60 at 0b4c88bbdf03 ↗

  10. hcard have (Finset.range (c j)).card ≤ (N + (1 : ℕ) + j).primeFactors.card

    Leaves c j ≤ (N + (1 : ℕ) + j).primeFactors.card, with hcard : (Finset.range (c j)).card ≤ (N + (1 : ℕ) + j).primeFactors.card.

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

    Lean, lines 62–63
      have hcard := Finset.card_le_card_of_injOn (s := Finset.range (c j))
    (t := (N + 1 + j).primeFactors) (fun i => q (j, i)) ?_ ?_

    targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, lines 62–63 at 0b4c88bbdf03 ↗

  11. s11 case

    Leaves c j ≤ (N + (1 : ℕ) + j).primeFactors.card.

    Lean, line 64
      · simpa using hcard

    targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, line 64 at 0b4c88bbdf03 ↗

  12. s12 case

    Leaves Set.MapsTo (fun (i : ℕ) => q (j, i)) (↑(Finset.range (c j)) : Set ℕ) (↑(N + (1 : ℕ) + j).primeFactors : Set ℕ).

    Uses library Nat.mem_primeFactors, And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

    Lean, lines 65–67
      · intro i hi
    have hi' : i < c j := Finset.mem_range.1 hi
    exact Nat.mem_primeFactors.2 ⟨hqp _, hdvd i hi', by omega⟩

    targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, lines 65–67 at 0b4c88bbdf03 ↗

    1. s12.hi' have i < c j

      Leaves (fun (i : ℕ) => q (j, i)) i ∈ (↑(N + (1 : ℕ) + j).primeFactors : Set ℕ), with hi' : i < c j.

      Uses library Finset.mem_range.

      Lean, line 66
          have hi' : i < c j := Finset.mem_range.1 hi

      targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, line 66 at 0b4c88bbdf03 ↗

  13. s13 case

    Leaves Set.InjOn (fun (i : ℕ) => q (j, i)) (↑(Finset.range (c j)) : Set ℕ).

    Lean, lines 68–70
      · intro i _ i' _ h
    have := hqinj h
    simpa using this

    targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, lines 68–70 at 0b4c88bbdf03 ↗

    1. s13.this have (j, i) = (j, i')

      Leaves i = i', with this : (j, i) = (j, i').

      Lean, line 69
          have := hqinj h

      targets/erdos-69/nodes/spec-7f0efe19/Proof.lean, line 69 at 0b4c88bbdf03 ↗

The proof in Lean (Proof.lean)

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

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

open scoped ArithmeticFunction.omega

/-! A speculative ingredient for erdos-69 (D-29): prescribed lower bounds for `ω` on a window of
consecutive integers. For every length `k` and every choice of lower bounds `c 0, …, c (k-1)`
there is `N` with `c j ≤ ω (N + 1 + j)` for each `j < k`: give each slot its own set of distinct
primes and solve the congruences by the Chinese remainder theorem. Rationality of
`∑ ω(n)/2^n` would make every tail `∑_{j ≥ 0} ω(N+1+j)/2^(j+1)` lie in a fixed lattice
`(1/b)ℤ`, and arguments against that (the literature route is Tao–Teräväinen, arXiv:2512.01739)
need windows whose `ω` values are controlled. This lemma is only the elementary, lower-bound
half of that control; the upper bounds, the hard part, are not here. -/

theorem Opn.erdos_69_omega_window :
    ∀ (k : ℕ) (c : ℕ → ℕ), ∃ N : ℕ, ∀ j < k, c j ≤ ω (N + 1 + j) := by
  intro k c
  -- one distinct prime `q (j, i)` for each slot `j < k` and each `i < c j`
  let q : ℕ × ℕ → ℕ := fun x => Nat.nth Nat.Prime (Nat.pair x.1 x.2)
  have hqp : ∀ x, (q x).Prime := fun x => Nat.prime_nth_prime _
  have hqinj : Function.Injective q := by
    intro x y h
    have h1 : Nat.pair x.1 x.2 = Nat.pair y.1 y.2 :=
      Nat.nth_injective Nat.infinite_setOfPred_prime h
    obtain ⟨h2, h3⟩ := Nat.pair_eq_pair.1 h1
    exact Prod.ext h2 h3
  let t : Finset (ℕ × ℕ) :=
    ((Finset.range k) ×ˢ (Finset.range ((Finset.range k).sup c))).filter (fun x => x.2 < c x.1)
  have hmem : ∀ j i, j < k → i < c j → (j, i) ∈ t := by
    intro j i hj hi
    simp only [t, Finset.mem_filter, Finset.mem_product, Finset.mem_range]
    refine ⟨⟨hj, lt_of_lt_of_le hi ?_⟩, hi⟩
    exact Finset.le_sup (f := c) (Finset.mem_range.2 hj)
  have ht : ∀ x ∈ t, x.1 < k := by
    intro x hx
    simp only [t, Finset.mem_filter, Finset.mem_product, Finset.mem_range] at hx
    exact hx.1.1
  have hq0 : ∀ x ∈ t, q x ≠ 0 := fun x _ => (hqp x).ne_zero
  have hcop : (↑t : Set (ℕ × ℕ)).Pairwise (Function.onFun Nat.Coprime q) := by
    intro x _ y _ hxy
    exact (Nat.coprime_primes (hqp x) (hqp y)).2 (hqinj.ne hxy)
  let a : ℕ × ℕ → ℕ := fun x => (k + 1) * q x - (1 + x.1)
  obtain ⟨N, hN⟩ := Nat.chineseRemainderOfFinset a q t hq0 hcop
  refine ⟨N, fun j hj => ?_⟩
  have hdvd : ∀ i < c j, q (j, i) ∣ N + 1 + j := by
    intro i hi
    have hx := hmem j i hj hi
    have h1 : N ≡ a (j, i) [MOD q (j, i)] := hN _ hx
    have h2 : 1 + j ≤ (k + 1) * q (j, i) := by
      have : 2 ≤ q (j, i) := (hqp _).two_le
      nlinarith
    have h3 : N + (1 + j) ≡ (k + 1) * q (j, i) [MOD q (j, i)] := by
      have := h1.add_right (1 + j)
      simpa [a, Nat.sub_add_cancel h2] using this
    have h4 : (k + 1) * q (j, i) ≡ 0 [MOD q (j, i)] :=
      (Nat.modEq_zero_iff_dvd).2 (dvd_mul_left _ _)
    have h5 := (Nat.modEq_zero_iff_dvd).1 (h3.trans h4)
    simpa [add_assoc] using h5
  have hω : ω (N + 1 + j) = (N + 1 + j).primeFactors.card := by
    rw [ArithmeticFunction.cardDistinctFactors_apply, Nat.primeFactors, List.card_toFinset]
  rw [hω]
  have hcard := Finset.card_le_card_of_injOn (s := Finset.range (c j))
    (t := (N + 1 + j).primeFactors) (fun i => q (j, i)) ?_ ?_
  · simpa using hcard
  · intro i hi
    have hi' : i < c j := Finset.mem_range.1 hi
    exact Nat.mem_primeFactors.2 ⟨hqp _, hdvd i hi', by omega⟩
  · intro i _ i' _ h
    have := hqinj h
    simpa using this

What is known

Work on it

No explainer yet. This proof written as a journal would print it, labelled unverified, is the next thing a writer could add, by pull request (D-3, D-36; the guide shows how).

Write the explainer →

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

Record

Statement: the Lean file and its words (1 version)

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-7f0efe19».Context

open scoped ArithmeticFunction.omega

/-! A speculative ingredient for erdos-69 (D-29): prescribed lower bounds for `ω` on a window of
consecutive integers. For every length `k` and every choice of lower bounds `c 0, …, c (k-1)`
there is `N` with `c j ≤ ω (N + 1 + j)` for each `j < k`: give each slot its own set of distinct
primes and solve the congruences by the Chinese remainder theorem. Rationality of
`∑ ω(n)/2^n` would make every tail `∑_{j ≥ 0} ω(N+1+j)/2^(j+1)` lie in a fixed lattice
`(1/b)ℤ`, and arguments against that (the literature route is Tao–Teräväinen, arXiv:2512.01739)
need windows whose `ω` values are controlled. This lemma is only the elementary, lower-bound
half of that control; the upper bounds, the hard part, are not here. -/

theorem Opn.erdos_69_omega_window :
    ∀ (k : ℕ) (c : ℕ → ℕ), ∃ N : ℕ, ∀ j < k, c j ≤ ω (N + 1 + j) := 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 k\in\mathbb{N},\ \forall c:\mathbb{N}\to\mathbb{N}\ \ \exists N\in\mathbb{N}\ \ \forall j<k:\quad c(j) \le \omega(N+1+j)$

For every length k and every sequence of naturals c there is a natural N with c(j) ≤ ω(N+1+j) for each j < k, where ω(n) is the number of distinct prime factors of n.

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

Rendered from targets/erdos-69/nodes/spec-7f0efe19/Statement.lean. Origin: authored.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000301.json, merge commit 0b4c88bbdf03.

Verdict pass, from attestations/000301.json.

Submitter
t0929-3
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/000301.json, merge commit 0b4c88bbdf03.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-69/nodes/spec-7f0efe19/Witness.lean, sha256 c12e03295ecf.
import Mathlib

open scoped ArithmeticFunction.omega

theorem witness : ∃ (k : ℕ) (c : ℕ → ℕ), True := ⟨0, fun _ => 0, trivial⟩

No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →

How to read this page

How to read a statement’s page →