New Mersenne conjecture

Reference: Wikipedia

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

A Mersenne prime is a prime number of the form 2ᵖ-1.

Equations

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

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

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

Equations

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

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

Holds when there is exists a number k such that p = 2ᵏ±1 or p = 4ᵏ±3.

Equations

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

def NewMersenne.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ᵖ-1 is prime
2. (2ᵖ+1)/3 is prime
3. Exists a number k such that p = 2ᵏ±1 or p = 4ᵏ±3

Equations

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

theorem NewMersenne.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ᵖ-1 is prime
2. (2ᵖ+1)/3 is prime
3. Exists a number k such that p = 2ᵏ±1 or p = 4ᵏ±3

theorem NewMersenne.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 NewMersenne.new_mersenne_conjecture.variants.prime (p : ℕ) (hp : Nat.Prime p) : NewMersenneConjectureStatement p