FormalConjectures.Wikipedia.FortuneConjecture

FormalConjectures
Wikipedia
FortuneConjecture

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Fortune's Conjecture

A Fortunate number is the smallest integer $m > 1$ such that $p_n\# + m$ is prime, where $p_n\#$ denotes the primorial of the $n$-th prime — equivalently, the product of the first $n$ primes.

Fortune's Conjecture asserts that every Fortunate number is prime — equivalently, that no Fortunate number is composite.

The conjecture is named after the social anthropologist Reo Fortune, who proposed it. The first few Fortunate numbers are $3, 5, 7, 13, 23, 17, 19, 23, 37, 61, \ldots$ (OEIS A005235); all known values are prime.

References:

Wikipedia

OEIS A005235

PrimePages glossary entry

PlanetMath: Fortune's conjecture

namespace FortuneConjectureopen Nat

For any natural number N there is some m > 1 with N + m prime; an immediate consequence of the infinitude of primes.


@[category API, AMS 11]
lemma exists_one_lt_prime_add (N : ℕ) : ∃ m, 1 < m ∧ Nat.Prime (N + m) := byN:ℕ⊢ ∃ m, 1 < m ∧ Nat.Prime (N + m)
  obtain ⟨p, hp_ge, hp_prime⟩ := Nat.exists_infinite_primes (N + 2)N:ℕp:ℕhp_ge:N + 2 ≤ php_prime:Nat.Prime p⊢ ∃ m, 1 < m ∧ Nat.Prime (N + m)
  refine ⟨p - N, byN:ℕp:ℕhp_ge:N + 2 ≤ php_prime:Nat.Prime p⊢ 1 < p - N omegaAll goals completed! 🐙, ?_⟩
  have hsum : N + (p - N) = p := byN:ℕ⊢ ∃ m, 1 < m ∧ Nat.Prime (N + m)N:ℕp:ℕhp_ge:N + 2 ≤ php_prime:Nat.Prime phsum:N + (p - N) = p⊢ Nat.Prime (N + (p - N)) omegaN:ℕp:ℕhp_ge:N + 2 ≤ php_prime:Nat.Prime phsum:N + (p - N) = p⊢ Nat.Prime (N + (p - N))N:ℕp:ℕhp_ge:N + 2 ≤ php_prime:Nat.Prime phsum:N + (p - N) = p⊢ Nat.Prime (N + (p - N))
  rw [hsumN:ℕp:ℕhp_ge:N + 2 ≤ php_prime:Nat.Prime phsum:N + (p - N) = p⊢ Nat.Prime pN:ℕp:ℕhp_ge:N + 2 ≤ php_prime:Nat.Prime phsum:N + (p - N) = p⊢ Nat.Prime p]N:ℕp:ℕhp_ge:N + 2 ≤ php_prime:Nat.Prime phsum:N + (p - N) = p⊢ Nat.Prime p; exact hp_primeAll goals completed! 🐙

The $n$-th Fortunate number (0-indexed): the smallest integer $m > 1$ such that $p_{n+1}\# + m$ is prime.

Nat.nth Nat.Prime n is the $(n+1)$-st prime (0-indexed), and primorial p is the product of all primes $\le p$; when $p$ is the $(n+1)$-st prime this equals the product of the first $n+1$ primes. Thus fortunateNumber 0 corresponds to $F_1 = 3$ in the OEIS A005235 indexing.

noncomputable def fortunateNumber (n : ℕ) : ℕ :=
  Nat.find (exists_one_lt_prime_add (primorial (Nat.nth Nat.Prime n)))

fortunateNumber n is greater than $1$, and adding it to the primorial of the $(n+1)$-st prime yields a prime.

@[category API, AMS 11]
lemma fortunateNumber_spec (n : ℕ) :
    1 < fortunateNumber n ∧
      Nat.Prime (primorial (Nat.nth Nat.Prime n) + fortunateNumber n) :=
  Nat.find_spec (exists_one_lt_prime_add (primorial (Nat.nth Nat.Prime n)))

Minimality of fortunateNumber n: no smaller integer $m > 1$ makes primorial (Nat.nth Nat.Prime n) + m prime.

@[category API, AMS 11]
lemma fortunateNumber_le (n m : ℕ) (hm : 1 < m)
    (hp : Nat.Prime (primorial (Nat.nth Nat.Prime n) + m)) :
    fortunateNumber n ≤ m :=
  Nat.find_min' (exists_one_lt_prime_add (primorial (Nat.nth Nat.Prime n))) ⟨hm, hp⟩



-- The first four Fortunate numbers (OEIS A005235): 3, 5, 7, 13.

@[category API, AMS 11]
theorem fortunateNumber_zero : fortunateNumber 0 = 3 := by⊢ fortunateNumber 0 = 3
  have hp : primorial (Nat.nth Nat.Prime 0) = 2 := by
    rw [Nat.nth_prime_zero_eq_two⊢ primorial 2 = 2⊢ primorial 2 = 2hp:primorial (nth Nat.Prime 0) = 2⊢ fortunateNumber 0 = 3]⊢ primorial 2 = 2hp:primorial (nth Nat.Prime 0) = 2⊢ fortunateNumber 0 = 3; decidehp:primorial (nth Nat.Prime 0) = 2⊢ fortunateNumber 0 = 3hp:primorial (nth Nat.Prime 0) = 2⊢ fortunateNumber 0 = 3
  show Nat.find (exists_one_lt_prime_add (primorial (Nat.nth Nat.Prime 0))) = 3hp:primorial (nth Nat.Prime 0) = 2⊢ Nat.find ⋯ = 3
  rw [Nat.find_eq_iffhp:primorial (nth Nat.Prime 0) = 2⊢ (1 < 3 ∧ Nat.Prime (primorial (nth Nat.Prime 0) + 3)) ∧ ∀ n < 3, ¬(1 < n ∧ Nat.Prime (primorial (nth Nat.Prime 0) + n))hp:primorial (nth Nat.Prime 0) = 2⊢ (1 < 3 ∧ Nat.Prime (primorial (nth Nat.Prime 0) + 3)) ∧ ∀ n < 3, ¬(1 < n ∧ Nat.Prime (primorial (nth Nat.Prime 0) + n))]hp:primorial (nth Nat.Prime 0) = 2⊢ (1 < 3 ∧ Nat.Prime (primorial (nth Nat.Prime 0) + 3)) ∧ ∀ n < 3, ¬(1 < n ∧ Nat.Prime (primorial (nth Nat.Prime 0) + n))
  refine ⟨⟨byhp:primorial (nth Nat.Prime 0) = 2⊢ 1 < 3 norm_numAll goals completed! 🐙, ?_⟩, ?_⟩
  ·refine_1hp:primorial (nth Nat.Prime 0) = 2⊢ Nat.Prime (primorial (nth Nat.Prime 0) + 3) show Nat.Prime (primorial (Nat.nth Nat.Prime 0) + 3)refine_1hp:primorial (nth Nat.Prime 0) = 2⊢ Nat.Prime (primorial (nth Nat.Prime 0) + 3)
    rw [hprefine_1hp:primorial (nth Nat.Prime 0) = 2⊢ Nat.Prime (2 + 3)refine_1hp:primorial (nth Nat.Prime 0) = 2⊢ Nat.Prime (2 + 3)]refine_1hp:primorial (nth Nat.Prime 0) = 2⊢ Nat.Prime (2 + 3); norm_numAll goals completed! 🐙
  ·refine_2hp:primorial (nth Nat.Prime 0) = 2⊢ ∀ n < 3, ¬(1 < n ∧ Nat.Prime (primorial (nth Nat.Prime 0) + n)) rintro m hm ⟨hm1, hmp⟩refine_2hp:primorial (nth Nat.Prime 0) = 2m:ℕhm:m < 3hm1:1 < mhmp:Nat.Prime (primorial (nth Nat.Prime 0) + m)⊢ False
    rw [hprefine_2hp:primorial (nth Nat.Prime 0) = 2m:ℕhm:m < 3hm1:1 < mhmp:Nat.Prime (2 + m)⊢ Falserefine_2hp:primorial (nth Nat.Prime 0) = 2m:ℕhm:m < 3hm1:1 < mhmp:Nat.Prime (2 + m)⊢ False] at hmprefine_2hp:primorial (nth Nat.Prime 0) = 2m:ℕhm:m < 3hm1:1 < mhmp:Nat.Prime (2 + m)⊢ False
    interval_cases mrefine_2.«2»hp:primorial (nth Nat.Prime 0) = 2m:ℕhm:2 < 3hm1:1 < 2hmp:Nat.Prime (2 + 2)⊢ False
    norm_num at hmpAll goals completed! 🐙



@[category API, AMS 11]
theorem fortunateNumber_one : fortunateNumber 1 = 5 := by⊢ fortunateNumber 1 = 5
  have hp : primorial (Nat.nth Nat.Prime 1) = 6 := by
    rw [Nat.nth_prime_one_eq_three⊢ primorial 3 = 6⊢ primorial 3 = 6hp:primorial (nth Nat.Prime 1) = 6⊢ fortunateNumber 1 = 5]⊢ primorial 3 = 6hp:primorial (nth Nat.Prime 1) = 6⊢ fortunateNumber 1 = 5; decidehp:primorial (nth Nat.Prime 1) = 6⊢ fortunateNumber 1 = 5hp:primorial (nth Nat.Prime 1) = 6⊢ fortunateNumber 1 = 5
  show Nat.find (exists_one_lt_prime_add (primorial (Nat.nth Nat.Prime 1))) = 5hp:primorial (nth Nat.Prime 1) = 6⊢ Nat.find ⋯ = 5
  rw [Nat.find_eq_iffhp:primorial (nth Nat.Prime 1) = 6⊢ (1 < 5 ∧ Nat.Prime (primorial (nth Nat.Prime 1) + 5)) ∧ ∀ n < 5, ¬(1 < n ∧ Nat.Prime (primorial (nth Nat.Prime 1) + n))hp:primorial (nth Nat.Prime 1) = 6⊢ (1 < 5 ∧ Nat.Prime (primorial (nth Nat.Prime 1) + 5)) ∧ ∀ n < 5, ¬(1 < n ∧ Nat.Prime (primorial (nth Nat.Prime 1) + n))]hp:primorial (nth Nat.Prime 1) = 6⊢ (1 < 5 ∧ Nat.Prime (primorial (nth Nat.Prime 1) + 5)) ∧ ∀ n < 5, ¬(1 < n ∧ Nat.Prime (primorial (nth Nat.Prime 1) + n))
  refine ⟨⟨byhp:primorial (nth Nat.Prime 1) = 6⊢ 1 < 5 norm_numAll goals completed! 🐙, ?_⟩, ?_⟩
  ·refine_1hp:primorial (nth Nat.Prime 1) = 6⊢ Nat.Prime (primorial (nth Nat.Prime 1) + 5) show Nat.Prime (primorial (Nat.nth Nat.Prime 1) + 5)refine_1hp:primorial (nth Nat.Prime 1) = 6⊢ Nat.Prime (primorial (nth Nat.Prime 1) + 5)
    rw [hprefine_1hp:primorial (nth Nat.Prime 1) = 6⊢ Nat.Prime (6 + 5)refine_1hp:primorial (nth Nat.Prime 1) = 6⊢ Nat.Prime (6 + 5)]refine_1hp:primorial (nth Nat.Prime 1) = 6⊢ Nat.Prime (6 + 5); norm_numAll goals completed! 🐙
  ·refine_2hp:primorial (nth Nat.Prime 1) = 6⊢ ∀ n < 5, ¬(1 < n ∧ Nat.Prime (primorial (nth Nat.Prime 1) + n)) rintro m hm ⟨hm1, hmp⟩refine_2hp:primorial (nth Nat.Prime 1) = 6m:ℕhm:m < 5hm1:1 < mhmp:Nat.Prime (primorial (nth Nat.Prime 1) + m)⊢ False
    rw [hprefine_2hp:primorial (nth Nat.Prime 1) = 6m:ℕhm:m < 5hm1:1 < mhmp:Nat.Prime (6 + m)⊢ Falserefine_2hp:primorial (nth Nat.Prime 1) = 6m:ℕhm:m < 5hm1:1 < mhmp:Nat.Prime (6 + m)⊢ False] at hmprefine_2hp:primorial (nth Nat.Prime 1) = 6m:ℕhm:m < 5hm1:1 < mhmp:Nat.Prime (6 + m)⊢ False
    interval_cases mrefine_2.«2»hp:primorial (nth Nat.Prime 1) = 6m:ℕhm:2 < 5hm1:1 < 2hmp:Nat.Prime (6 + 2)⊢ Falserefine_2.«3»hp:primorial (nth Nat.Prime 1) = 6m:ℕhm:3 < 5hm1:1 < 3hmp:Nat.Prime (6 + 3)⊢ Falserefine_2.«4»hp:primorial (nth Nat.Prime 1) = 6m:ℕhm:4 < 5hm1:1 < 4hmp:Nat.Prime (6 + 4)⊢ False <;>refine_2.«2»hp:primorial (nth Nat.Prime 1) = 6m:ℕhm:2 < 5hm1:1 < 2hmp:Nat.Prime (6 + 2)⊢ Falserefine_2.«3»hp:primorial (nth Nat.Prime 1) = 6m:ℕhm:3 < 5hm1:1 < 3hmp:Nat.Prime (6 + 3)⊢ Falserefine_2.«4»hp:primorial (nth Nat.Prime 1) = 6m:ℕhm:4 < 5hm1:1 < 4hmp:Nat.Prime (6 + 4)⊢ False norm_num at hmpAll goals completed! 🐙



@[category API, AMS 11]
theorem fortunateNumber_two : fortunateNumber 2 = 7 := by⊢ fortunateNumber 2 = 7
  have hp : primorial (Nat.nth Nat.Prime 2) = 30 := by
    rw [Nat.nth_prime_two_eq_five⊢ primorial 5 = 30⊢ primorial 5 = 30hp:primorial (nth Nat.Prime 2) = 30⊢ fortunateNumber 2 = 7]⊢ primorial 5 = 30hp:primorial (nth Nat.Prime 2) = 30⊢ fortunateNumber 2 = 7; decidehp:primorial (nth Nat.Prime 2) = 30⊢ fortunateNumber 2 = 7hp:primorial (nth Nat.Prime 2) = 30⊢ fortunateNumber 2 = 7
  show Nat.find (exists_one_lt_prime_add (primorial (Nat.nth Nat.Prime 2))) = 7hp:primorial (nth Nat.Prime 2) = 30⊢ Nat.find ⋯ = 7
  rw [Nat.find_eq_iffhp:primorial (nth Nat.Prime 2) = 30⊢ (1 < 7 ∧ Nat.Prime (primorial (nth Nat.Prime 2) + 7)) ∧ ∀ n < 7, ¬(1 < n ∧ Nat.Prime (primorial (nth Nat.Prime 2) + n))hp:primorial (nth Nat.Prime 2) = 30⊢ (1 < 7 ∧ Nat.Prime (primorial (nth Nat.Prime 2) + 7)) ∧ ∀ n < 7, ¬(1 < n ∧ Nat.Prime (primorial (nth Nat.Prime 2) + n))]hp:primorial (nth Nat.Prime 2) = 30⊢ (1 < 7 ∧ Nat.Prime (primorial (nth Nat.Prime 2) + 7)) ∧ ∀ n < 7, ¬(1 < n ∧ Nat.Prime (primorial (nth Nat.Prime 2) + n))
  refine ⟨⟨byhp:primorial (nth Nat.Prime 2) = 30⊢ 1 < 7 norm_numAll goals completed! 🐙, ?_⟩, ?_⟩
  ·refine_1hp:primorial (nth Nat.Prime 2) = 30⊢ Nat.Prime (primorial (nth Nat.Prime 2) + 7) show Nat.Prime (primorial (Nat.nth Nat.Prime 2) + 7)refine_1hp:primorial (nth Nat.Prime 2) = 30⊢ Nat.Prime (primorial (nth Nat.Prime 2) + 7)
    rw [hprefine_1hp:primorial (nth Nat.Prime 2) = 30⊢ Nat.Prime (30 + 7)refine_1hp:primorial (nth Nat.Prime 2) = 30⊢ Nat.Prime (30 + 7)]refine_1hp:primorial (nth Nat.Prime 2) = 30⊢ Nat.Prime (30 + 7); norm_numAll goals completed! 🐙
  ·refine_2hp:primorial (nth Nat.Prime 2) = 30⊢ ∀ n < 7, ¬(1 < n ∧ Nat.Prime (primorial (nth Nat.Prime 2) + n)) rintro m hm ⟨hm1, hmp⟩refine_2hp:primorial (nth Nat.Prime 2) = 30m:ℕhm:m < 7hm1:1 < mhmp:Nat.Prime (primorial (nth Nat.Prime 2) + m)⊢ False
    rw [hprefine_2hp:primorial (nth Nat.Prime 2) = 30m:ℕhm:m < 7hm1:1 < mhmp:Nat.Prime (30 + m)⊢ Falserefine_2hp:primorial (nth Nat.Prime 2) = 30m:ℕhm:m < 7hm1:1 < mhmp:Nat.Prime (30 + m)⊢ False] at hmprefine_2hp:primorial (nth Nat.Prime 2) = 30m:ℕhm:m < 7hm1:1 < mhmp:Nat.Prime (30 + m)⊢ False
    interval_cases mrefine_2.«2»hp:primorial (nth Nat.Prime 2) = 30m:ℕhm:2 < 7hm1:1 < 2hmp:Nat.Prime (30 + 2)⊢ Falserefine_2.«3»hp:primorial (nth Nat.Prime 2) = 30m:ℕhm:3 < 7hm1:1 < 3hmp:Nat.Prime (30 + 3)⊢ Falserefine_2.«4»hp:primorial (nth Nat.Prime 2) = 30m:ℕhm:4 < 7hm1:1 < 4hmp:Nat.Prime (30 + 4)⊢ Falserefine_2.«5»hp:primorial (nth Nat.Prime 2) = 30m:ℕhm:5 < 7hm1:1 < 5hmp:Nat.Prime (30 + 5)⊢ Falserefine_2.«6»hp:primorial (nth Nat.Prime 2) = 30m:ℕhm:6 < 7hm1:1 < 6hmp:Nat.Prime (30 + 6)⊢ False <;>refine_2.«2»hp:primorial (nth Nat.Prime 2) = 30m:ℕhm:2 < 7hm1:1 < 2hmp:Nat.Prime (30 + 2)⊢ Falserefine_2.«3»hp:primorial (nth Nat.Prime 2) = 30m:ℕhm:3 < 7hm1:1 < 3hmp:Nat.Prime (30 + 3)⊢ Falserefine_2.«4»hp:primorial (nth Nat.Prime 2) = 30m:ℕhm:4 < 7hm1:1 < 4hmp:Nat.Prime (30 + 4)⊢ Falserefine_2.«5»hp:primorial (nth Nat.Prime 2) = 30m:ℕhm:5 < 7hm1:1 < 5hmp:Nat.Prime (30 + 5)⊢ Falserefine_2.«6»hp:primorial (nth Nat.Prime 2) = 30m:ℕhm:6 < 7hm1:1 < 6hmp:Nat.Prime (30 + 6)⊢ False norm_num at hmpAll goals completed! 🐙



@[category API, AMS 11]
theorem fortunateNumber_three : fortunateNumber 3 = 13 := by⊢ fortunateNumber 3 = 13
  have hp : primorial (Nat.nth Nat.Prime 3) = 210 := by
    rw [Nat.nth_prime_three_eq_seven⊢ primorial 7 = 210⊢ primorial 7 = 210hp:primorial (nth Nat.Prime 3) = 210⊢ fortunateNumber 3 = 13]⊢ primorial 7 = 210hp:primorial (nth Nat.Prime 3) = 210⊢ fortunateNumber 3 = 13; decidehp:primorial (nth Nat.Prime 3) = 210⊢ fortunateNumber 3 = 13hp:primorial (nth Nat.Prime 3) = 210⊢ fortunateNumber 3 = 13
  show Nat.find (exists_one_lt_prime_add (primorial (Nat.nth Nat.Prime 3))) = 13hp:primorial (nth Nat.Prime 3) = 210⊢ Nat.find ⋯ = 13
  rw [Nat.find_eq_iffhp:primorial (nth Nat.Prime 3) = 210⊢ (1 < 13 ∧ Nat.Prime (primorial (nth Nat.Prime 3) + 13)) ∧
  ∀ n < 13, ¬(1 < n ∧ Nat.Prime (primorial (nth Nat.Prime 3) + n))hp:primorial (nth Nat.Prime 3) = 210⊢ (1 < 13 ∧ Nat.Prime (primorial (nth Nat.Prime 3) + 13)) ∧
  ∀ n < 13, ¬(1 < n ∧ Nat.Prime (primorial (nth Nat.Prime 3) + n))]hp:primorial (nth Nat.Prime 3) = 210⊢ (1 < 13 ∧ Nat.Prime (primorial (nth Nat.Prime 3) + 13)) ∧
  ∀ n < 13, ¬(1 < n ∧ Nat.Prime (primorial (nth Nat.Prime 3) + n))
  refine ⟨⟨byhp:primorial (nth Nat.Prime 3) = 210⊢ 1 < 13 norm_numAll goals completed! 🐙, ?_⟩, ?_⟩
  ·refine_1hp:primorial (nth Nat.Prime 3) = 210⊢ Nat.Prime (primorial (nth Nat.Prime 3) + 13) show Nat.Prime (primorial (Nat.nth Nat.Prime 3) + 13)refine_1hp:primorial (nth Nat.Prime 3) = 210⊢ Nat.Prime (primorial (nth Nat.Prime 3) + 13)
    rw [hprefine_1hp:primorial (nth Nat.Prime 3) = 210⊢ Nat.Prime (210 + 13)refine_1hp:primorial (nth Nat.Prime 3) = 210⊢ Nat.Prime (210 + 13)]refine_1hp:primorial (nth Nat.Prime 3) = 210⊢ Nat.Prime (210 + 13); norm_numAll goals completed! 🐙
  ·refine_2hp:primorial (nth Nat.Prime 3) = 210⊢ ∀ n < 13, ¬(1 < n ∧ Nat.Prime (primorial (nth Nat.Prime 3) + n)) rintro m hm ⟨hm1, hmp⟩refine_2hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:m < 13hm1:1 < mhmp:Nat.Prime (primorial (nth Nat.Prime 3) + m)⊢ False
    rw [hprefine_2hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:m < 13hm1:1 < mhmp:Nat.Prime (210 + m)⊢ Falserefine_2hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:m < 13hm1:1 < mhmp:Nat.Prime (210 + m)⊢ False] at hmprefine_2hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:m < 13hm1:1 < mhmp:Nat.Prime (210 + m)⊢ False
    interval_cases mrefine_2.«2»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:2 < 13hm1:1 < 2hmp:Nat.Prime (210 + 2)⊢ Falserefine_2.«3»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:3 < 13hm1:1 < 3hmp:Nat.Prime (210 + 3)⊢ Falserefine_2.«4»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:4 < 13hm1:1 < 4hmp:Nat.Prime (210 + 4)⊢ Falserefine_2.«5»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:5 < 13hm1:1 < 5hmp:Nat.Prime (210 + 5)⊢ Falserefine_2.«6»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:6 < 13hm1:1 < 6hmp:Nat.Prime (210 + 6)⊢ Falserefine_2.«7»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:7 < 13hm1:1 < 7hmp:Nat.Prime (210 + 7)⊢ Falserefine_2.«8»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:8 < 13hm1:1 < 8hmp:Nat.Prime (210 + 8)⊢ Falserefine_2.«9»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:9 < 13hm1:1 < 9hmp:Nat.Prime (210 + 9)⊢ Falserefine_2.«10»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:10 < 13hm1:1 < 10hmp:Nat.Prime (210 + 10)⊢ Falserefine_2.«11»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:11 < 13hm1:1 < 11hmp:Nat.Prime (210 + 11)⊢ Falserefine_2.«12»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:12 < 13hm1:1 < 12hmp:Nat.Prime (210 + 12)⊢ False <;>refine_2.«2»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:2 < 13hm1:1 < 2hmp:Nat.Prime (210 + 2)⊢ Falserefine_2.«3»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:3 < 13hm1:1 < 3hmp:Nat.Prime (210 + 3)⊢ Falserefine_2.«4»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:4 < 13hm1:1 < 4hmp:Nat.Prime (210 + 4)⊢ Falserefine_2.«5»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:5 < 13hm1:1 < 5hmp:Nat.Prime (210 + 5)⊢ Falserefine_2.«6»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:6 < 13hm1:1 < 6hmp:Nat.Prime (210 + 6)⊢ Falserefine_2.«7»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:7 < 13hm1:1 < 7hmp:Nat.Prime (210 + 7)⊢ Falserefine_2.«8»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:8 < 13hm1:1 < 8hmp:Nat.Prime (210 + 8)⊢ Falserefine_2.«9»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:9 < 13hm1:1 < 9hmp:Nat.Prime (210 + 9)⊢ Falserefine_2.«10»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:10 < 13hm1:1 < 10hmp:Nat.Prime (210 + 10)⊢ Falserefine_2.«11»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:11 < 13hm1:1 < 11hmp:Nat.Prime (210 + 11)⊢ Falserefine_2.«12»hp:primorial (nth Nat.Prime 3) = 210m:ℕhm:12 < 13hm1:1 < 12hmp:Nat.Prime (210 + 12)⊢ False norm_num at hmpAll goals completed! 🐙

Fortune's Conjecture: Every Fortunate number is prime.

@[category research open, AMS 11]
theorem fortune_conjecture :
    answer(sorry) ↔ (∀ n : ℕ, Nat.Prime (fortunateNumber n)) := by⊢ True ↔ ∀ (n : ℕ), Nat.Prime (fortunateNumber n)
  sorryAll goals completed! 🐙

end FortuneConjecture