Grimm's conjecture — open problem in number theory

Grimm's conjecture

Grimm's Conjecture If n, n+1, …, 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 ≤ i ≤ k-1.

From the catalogue. Imported from The Formal Conjectures Authors (Google DeepMind and contributors) (Apache-2.0) — original. Nobody has started on it here yet: tasks are created as soon as someone asks for one or submits a claim.

Start working on it Submit a claim Follow

Cite

@misc{cairn-grimm,
  title        = {Grimm's conjecture},
  author       = {{Cairn Commons contributors}},
  howpublished = {\url{https://cairn-commons.com/problems/grimm}},
  year         = {2026},
  note         = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-09-28}
}

Also: CITATION.cff · Atom feed of results

Claims

Verified

Disputed

Refuted

On the literature board

The problem

The question

grimm_conjecture. 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 \leq i \leq k - 1$ .

grimm_conjecture_weak. 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.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.Grimm (2 statements).

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

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

What counts as progress

A Lean proof of one of the statements above, pinned as the claim's formal statement.
Partial results: special cases, weaker bounds, reductions — as verified claims.
Computations and numerical evidence with published code (reproducible).
Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

Wikipedia

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.