Grimm's conjecture

Reference: Wikipedia

theorem Grimm.grimm_conjecture (n k : ℕ) (hn : 1 ≤ n) (hk : 1 ≤ k) (h : ∀ (i : Fin k), 1 < n + ↑i ∧ ¬Nat.Prime (n + ↑i)) : ∃ (ps : Fin k ↪ ℕ), ∀ (i : Fin k), Nat.Prime (ps i) ∧ ps i ∣ n + ↑i

Grimm's Conjecture If $n, n+1, \dots, n+k-1$ are all composite numbers, then there are $k$ distinct primes $p_i$ such that $p_i$ divides $n + i$ for all $0 \le i \le k-1$.

theorem Grimm.grimm_conjecture_weak (n k : ℕ) (hn : 1 ≤ n) (hk : 1 ≤ k) (h : ∀ (i : Fin k), 1 < n + ↑i ∧ ¬Nat.Prime (n + ↑i)) : ∃ (ps : Fin k ↪ ℕ), ∀ (i : Fin k), Nat.Prime (ps i) ∧ ∃ (j : Fin k), ps i ∣ n + ↑j

Grimm's Conjecture, weaker version If $n, n+1, \dots, n+k-1$ are all composite numbers, then their product has at least $k$ distinct prime divisors.