What is the conjecture
A Fortunate number is the smallest integer $m > 1$ such that $pr_n + m$ is prime, where $pr_n$ denotes the primorial (the product of the first $n$ prime numbers).
Fortune's conjecture states that no Fortunate number is composite, equivalently, that every Fortunate number is prime.
(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)
Sources:
Prerequisites needed
Formalizability Rating: 1/5 (0 is best) (as of 2026-04-03)
Building blocks (1-3; from search results):
Nat.Prime and Prime predicate (Mathlib.Algebra.Prime.Defs)primorial function (Mathlib.NumberTheory.Primorial)- Standard arithmetic on natural numbers
Missing pieces (exactly 2; unclear/absent from search results):
- Definition of
fortunate_number : ℕ → ℕ as the smallest m > 1 such that primorial n + m is prime
- Lemma relating primality of individual Fortunate numbers to the conjecture statement
Rating justification (1-2 sentences): The core building blocks (primorial and prime predicates) exist in Mathlib, requiring only a straightforward definition of the fortunate_number function. The conjecture statement can be formulated immediately using existing Mathlib definitions.
Choose either option
This issue was generated by an AI agent and reviewed by me.
If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: link
What is the conjecture
A Fortunate number is the smallest integer$m > 1$ such that $pr_n + m$ is prime, where $pr_n$ denotes the primorial (the product of the first $n$ prime numbers).
Fortune's conjecture states that no Fortunate number is composite, equivalently, that every Fortunate number is prime.
(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)
Sources:
Prerequisites needed
Formalizability Rating: 1/5 (0 is best) (as of 2026-04-03)
Building blocks (1-3; from search results):
Nat.PrimeandPrimepredicate (Mathlib.Algebra.Prime.Defs)primorialfunction (Mathlib.NumberTheory.Primorial)Missing pieces (exactly 2; unclear/absent from search results):
fortunate_number : ℕ → ℕas the smallest m > 1 such that primorial n + m is primeRating justification (1-2 sentences): The core building blocks (primorial and prime predicates) exist in Mathlib, requiring only a straightforward definition of the fortunate_number function. The conjecture statement can be formulated immediately using existing Mathlib definitions.
AMS categories
Choose either option
This issue was generated by an AI agent and reviewed by me.
If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: link