Conjectures about Mersenne primes

References:

• Wikipedia: Mersenne conjectures
• Wikipedia: Catalan's Mersenne conjecture
• MathWorld: Catalan-Mersenne Number

def Mersenne.Nat.GivesWagstaffPrime (p : ℕ) : Prop

A Wagstaff prime is a prime number of the form $(2^p+1)/3$.

Equations

• Mersenne.Nat.GivesWagstaffPrime p = (Odd p ∧ Nat.Prime ((2 ^ p + 1) / 3))

def Mersenne.Nat.IsSpecialForm (p : ℕ) : Prop

Holds when there is exists a number k such that $p = 2^k \\pm 1$ or $p = 4^k \\pm 3$.

Equations

• Mersenne.Nat.IsSpecialForm p = ∃ (k : ℕ), p = 2 ^ k + 1 ∨ p = 2 ^ k - 1 ∨ p = 4 ^ k + 3 ∨ p = 4 ^ k - 3

def Mersenne.catalanMersenne : ℕ → ℕ

The Catalan-Mersenne numbers, defined recursively by $c_0 = 2$ and $c_{n+1} = 2^{c_n} - 1$.

Equations

• Mersenne.catalanMersenne 0 = 2
• Mersenne.catalanMersenne n.succ = 2 ^ Mersenne.catalanMersenne n - 1

def Mersenne.NewMersenneConjectureStatement (p : ℕ) : Prop

A natural number p satisfies the statement of the New Mersenne Conjecture if whenever two of the following conditions hold, then all three must hold:

1. $2^p-1$ is prime
2. $(2^p+1)/3$ is prime
3. Exists a number k such that $p = 2^k \\pm 1$ or $p = 4^k \\pm 3$

Equations

• One or more equations did not get rendered due to their size.

theorem Mersenne.new_mersenne_conjecture (p : ℕ) (hp : Odd p) : NewMersenneConjectureStatement p

For any odd natural number p if two of the following conditions hold, then all three must hold:

1. $2^p-1$ is prime
2. $(2^p+1)/3$ is prime
3. Exists a number k such that $p = 2^k \\pm 1$ or $p = 4^k \\pm 3$

theorem Mersenne.new_mersenne_conjecture_of_prime : (∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement p) → ∀ (p : ℕ), Odd p → NewMersenneConjectureStatement p

It suffices to check this conjecture for primes

theorem Mersenne.new_mersenne_conjecture.variants.prime (p : ℕ) (hp : Nat.Prime p) (h : Odd p) : NewMersenneConjectureStatement p

The New Mersenne Conjecture statement holds for odd primes.

theorem Mersenne.infinitely_many_mersenne_primes : True ↔ {p : ℕ | Nat.Prime (mersenne p)}.Infinite

Are there infinitely many Mersenne primes?

theorem Mersenne.catalans_mersenne_conjecture : True ↔ ∀ n ≥ 5, Nat.Prime (catalanMersenne n)

The first five Catalan-Mersenne numbers $c_0, \ldots, c_4$ are known to be prime. Catalan conjectured that they are prime "up to a certain limit". Are all Catalan-Mersenne numbers $c_n$ with $n \geq 5$ prime?