Conjectures about Mersenne primes

Reference: Wikipedia

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

A Mersenne prime is a prime number of the form $2^p-1$.

Equations

• Mersenne.Nat.GivesMersennePrime p = Nat.Prime (2 ^ p - 1)

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.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) : NewMersenneConjectureStatement p

theorem Mersenne.infinitely_many_mersenne_primes : {p : ℕ | Nat.GivesMersennePrime p}.Infinite ↔ sorry

Are there infinitely many Mersenne primes?