1. FormalConjectures
  2. Wikipedia
  3. Mersenne
/- Copyright 2025 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

Conjectures about Mersenne primes

References:

namespace Mersenne namespace Nat

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

def GivesWagstaffPrime (p : ℕ) : Prop := Odd p ∧ Nat.Prime ((2^p + 1) / 3)

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

def IsSpecialForm (p : ℕ) : Prop := ∃ k : ℕ, p = 2^k + 1 ∨ p = 2^k - 1 ∨ p = 4^k + 3 ∨ p = 4^k - 3 end Nat open Mersenne

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

def catalanMersenne : ℕ → ℕ | 0 => 2 | n + 1 => 2 ^ catalanMersenne n - 1

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:

    $2^p-1$ is prime

    $(2^p+1)/3$ is prime

    Exists a number k such that $p = 2^k \pm 1$ or $p = 4^k \pm 3$

def NewMersenneConjectureStatement (p : ℕ) : Prop := ((mersenne p).Prime ∧ p.GivesWagstaffPrime → p.IsSpecialForm) ∧ ((mersenne p).Prime ∧ p.IsSpecialForm → p.GivesWagstaffPrime) ∧ (p.GivesWagstaffPrime ∧ p.IsSpecialForm → (mersenne p).Prime)

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

    $2^p-1$ is prime

    $(2^p+1)/3$ is prime

    Exists a number k such that $p = 2^k \pm 1$ or $p = 4^k \pm 3$

@[category research open, AMS 11] theorem declaration uses 'sorry'new_mersenne_conjecture (p : ℕ) (hp : Odd p) : NewMersenneConjectureStatement p := p:ℕhp:Odd p⊢ NewMersenneConjectureStatement p All goals completed! 🐙

It suffices to check this conjecture for primes

@[category textbook, AMS 11] theorem new_mersenne_conjecture_of_prime : (∀ p, p.Prime → NewMersenneConjectureStatement p) → ∀ p, Odd p → NewMersenneConjectureStatement p := ⊢ (∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement p) → ∀ (p : ℕ), Odd p → NewMersenneConjectureStatement p intro H H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕ⊢ Odd p → NewMersenneConjectureStatement p H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd p⊢ NewMersenneConjectureStatement p H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:Nat.Prime p⊢ NewMersenneConjectureStatement pH:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime p⊢ NewMersenneConjectureStatement p H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:Nat.Prime p⊢ NewMersenneConjectureStatement p All goals completed! 🐙 suffices ¬Nat.GivesWagstaffPrime p H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pthis:¬Nat.GivesWagstaffPrime p := ?m.24⊢ NewMersenneConjectureStatement p H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pthis:¬Nat.GivesWagstaffPrime p := ?m.24hF1:¬Nat.Prime (mersenne p) := fun h => hp_prime (Nat.Prime.of_mersenne h)⊢ NewMersenneConjectureStatement p H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pthis:¬Nat.GivesWagstaffPrime p := ?m.24hF1:¬Nat.Prime (mersenne p) := fun h => hp_prime (Nat.Prime.of_mersenne h)⊢ Nat.Prime (mersenne p) ∧ Nat.GivesWagstaffPrime p → Nat.IsSpecialForm pH:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pthis:¬Nat.GivesWagstaffPrime p := ?m.24hF1:¬Nat.Prime (mersenne p) := fun h => hp_prime (Nat.Prime.of_mersenne h)⊢ Nat.Prime (mersenne p) ∧ Nat.IsSpecialForm p → Nat.GivesWagstaffPrime pH:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pthis:¬Nat.GivesWagstaffPrime p := ?m.24hF1:¬Nat.Prime (mersenne p) := fun h => hp_prime (Nat.Prime.of_mersenne h)⊢ Nat.GivesWagstaffPrime p ∧ Nat.IsSpecialForm p → Nat.Prime (mersenne p) H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pthis:¬Nat.GivesWagstaffPrime p := ?m.24hF1:¬Nat.Prime (mersenne p) := fun h => hp_prime (Nat.Prime.of_mersenne h)⊢ Nat.Prime (mersenne p) ∧ Nat.GivesWagstaffPrime p → Nat.IsSpecialForm pH:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pthis:¬Nat.GivesWagstaffPrime p := ?m.24hF1:¬Nat.Prime (mersenne p) := fun h => hp_prime (Nat.Prime.of_mersenne h)⊢ Nat.Prime (mersenne p) ∧ Nat.IsSpecialForm p → Nat.GivesWagstaffPrime pH:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pthis:¬Nat.GivesWagstaffPrime p := ?m.24hF1:¬Nat.Prime (mersenne p) := fun h => hp_prime (Nat.Prime.of_mersenne h)⊢ Nat.GivesWagstaffPrime p ∧ Nat.IsSpecialForm p → Nat.Prime (mersenne p) All goals completed! 🐙 H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)⊢ False H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:p = 1⊢ FalseH:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1⊢ False H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:p = 1⊢ False All goals completed! 🐙 H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFac⊢ False H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_dvd:q ∣ p := Nat.minFac_dvd p⊢ False H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_dvd:q ∣ p := Nat.minFac_dvd phq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ hq_dvd))⊢ False H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_dvd:q ∣ p := Nat.minFac_dvd phq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ hq_dvd))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2⊢ False H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ hq_dvd))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * s⊢ False H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ hq_dvd))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * shs_odd:Odd s := (Nat.odd_mul.mp (hs ▸ hp_odd)).right⊢ False have hpow_dvd : 2 ^ q + 1 ∣ 2 ^ p + 1 := ⊢ (∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement p) → ∀ (p : ℕ), Odd p → NewMersenneConjectureStatement p All goals completed! 🐙 have h3q : 3 ∣ 2 ^ q + 1 := ⊢ (∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement p) → ∀ (p : ℕ), Odd p → NewMersenneConjectureStatement p All goals completed! 🐙 H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ hq_dvd))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * shs_odd:Odd s := (Nat.odd_mul.mp (hs ▸ hp_odd)).righthpow_dvd:2 ^ q + 1 ∣ 2 ^ p + 1 := new_mersenne_conjecture_of_prime._proof_5 p s hs hs_oddh3q:3 ∣ 2 ^ q + 1 := new_mersenne_conjecture_of_prime._proof_6 p hq_oddh3p:3 ∣ 2 ^ p + 1 := Dvd.dvd.trans h3q hpow_dvd⊢ False H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ hq_dvd))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * shs_odd:Odd s := (Nat.odd_mul.mp (hs ▸ hp_odd)).righth3q:3 ∣ 2 ^ q + 1 := new_mersenne_conjecture_of_prime._proof_6 p hq_oddh3p:3 ∣ 2 ^ p + 1 := Dvd.dvd.trans h3q hpow_dvdk:ℕhk:2 ^ p + 1 = (2 ^ q + 1) * k⊢ False H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ hq_dvd))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * shs_odd:Odd s := (Nat.odd_mul.mp (hs ▸ hp_odd)).righth3q:3 ∣ 2 ^ q + 1 := new_mersenne_conjecture_of_prime._proof_6 p hq_oddh3p:3 ∣ 2 ^ p + 1 := Dvd.dvd.trans h3q hpow_dvdk:ℕhk:2 ^ p + 1 = (2 ^ q + 1) * kd:ℕ := (2 ^ q + 1) / 3hd:d = (2 ^ q + 1) / 3 := rfl⊢ False have hd_dvd : d ∣ (2 ^ p + 1) / 3 := ⊢ (∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement p) → ∀ (p : ℕ), Odd p → NewMersenneConjectureStatement p H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ hq_dvd))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * shs_odd:Odd s := (Nat.odd_mul.mp (hs ▸ hp_odd)).righth3q:3 ∣ 2 ^ q + 1 := new_mersenne_conjecture_of_prime._proof_6 p hq_oddh3p:3 ∣ 2 ^ p + 1 := Dvd.dvd.trans h3q hpow_dvdk:ℕhk:2 ^ p + 1 = (2 ^ q + 1) * kd:ℕ := (2 ^ q + 1) / 3hd:d = (2 ^ q + 1) / 3 := rfl⊢ (2 ^ p + 1) / 3 = d * k All goals completed! 🐙 have h8 : 8 ≤ 2 ^ q := ⊢ (∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement p) → ∀ (p : ℕ), Odd p → NewMersenneConjectureStatement p calc 8 = 2 ^ 3 := H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ _fvar.12184))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * shs_odd:Odd s := (Nat.odd_mul.mp (hs ▸ hp_odd)).righth3q:3 ∣ 2 ^ q + 1 := new_mersenne_conjecture_of_prime._proof_6 p hq_oddh3p:3 ∣ 2 ^ p + 1 := Dvd.dvd.trans h3q _fvar.14979k:ℕhk:2 ^ p + 1 = (2 ^ q + 1) * kd:ℕ := (2 ^ q + 1) / 3hd:d = (2 ^ q + 1) / 3 := rflhd_dvd:d ∣ (2 ^ p + 1) / 3 := Exists.intro k (new_mersenne_conjecture_of_prime._proof_7 p h3q k hk)⊢ 8 = 2 ^ 3 All goals completed! 🐙 _ ≤ 2 ^ q := Nat.pow_le_pow_right (H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ _fvar.12184))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * shs_odd:Odd s := (Nat.odd_mul.mp (hs ▸ hp_odd)).righth3q:3 ∣ 2 ^ q + 1 := new_mersenne_conjecture_of_prime._proof_6 p hq_oddh3p:3 ∣ 2 ^ p + 1 := Dvd.dvd.trans h3q _fvar.14979k:ℕhk:2 ^ p + 1 = (2 ^ q + 1) * kd:ℕ := (2 ^ q + 1) / 3hd:d = (2 ^ q + 1) / 3 := rflhd_dvd:d ∣ (2 ^ p + 1) / 3 := Exists.intro k (new_mersenne_conjecture_of_prime._proof_7 p h3q k hk)⊢ 2 > 0 All goals completed! 🐙) (H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ _fvar.12184))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * shs_odd:Odd s := (Nat.odd_mul.mp (hs ▸ hp_odd)).righth3q:3 ∣ 2 ^ q + 1 := new_mersenne_conjecture_of_prime._proof_6 p hq_oddh3p:3 ∣ 2 ^ p + 1 := Dvd.dvd.trans h3q _fvar.14979k:ℕhk:2 ^ p + 1 = (2 ^ q + 1) * kd:ℕ := (2 ^ q + 1) / 3hd:d = (2 ^ q + 1) / 3 := rflhd_dvd:d ∣ (2 ^ p + 1) / 3 := Exists.intro k (new_mersenne_conjecture_of_prime._proof_7 p h3q k hk)⊢ 3 ≤ q All goals completed! 🐙) have hd_lt : d < (2 ^ p + 1) / 3 := ⊢ (∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement p) → ∀ (p : ℕ), Odd p → NewMersenneConjectureStatement p have hpow : 2 ^ q < 2 ^ p := ⊢ (∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement p) → ∀ (p : ℕ), Odd p → NewMersenneConjectureStatement p H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ hq_dvd))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * shs_odd:Odd s := (Nat.odd_mul.mp (hs ▸ hp_odd)).righth3q:3 ∣ 2 ^ q + 1 := new_mersenne_conjecture_of_prime._proof_6 p hq_oddh3p:3 ∣ 2 ^ p + 1 := Dvd.dvd.trans h3q hpow_dvdk:ℕhk:2 ^ p + 1 = (2 ^ q + 1) * kd:ℕ := (2 ^ q + 1) / 3hd:d = (2 ^ q + 1) / 3 := rflhd_dvd:d ∣ (2 ^ p + 1) / 3 := Exists.intro k (new_mersenne_conjecture_of_prime._proof_7 p h3q k hk)h8:8 ≤ 2 ^ q := Trans.trans (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8)) (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)) (Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit1))) (Nat.pow_le_pow_right (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)) (new_mersenne_conjecture_of_prime._proof_8 p hp1 hq_ne2))⊢ 1 < 2H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ hq_dvd))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * shs_odd:Odd s := (Nat.odd_mul.mp (hs ▸ hp_odd)).righth3q:3 ∣ 2 ^ q + 1 := new_mersenne_conjecture_of_prime._proof_6 p hq_oddh3p:3 ∣ 2 ^ p + 1 := Dvd.dvd.trans h3q hpow_dvdk:ℕhk:2 ^ p + 1 = (2 ^ q + 1) * kd:ℕ := (2 ^ q + 1) / 3hd:d = (2 ^ q + 1) / 3 := rflhd_dvd:d ∣ (2 ^ p + 1) / 3 := Exists.intro k (new_mersenne_conjecture_of_prime._proof_7 p h3q k hk)h8:8 ≤ 2 ^ q := Trans.trans (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8)) (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)) (Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit1))) (Nat.pow_le_pow_right (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)) (new_mersenne_conjecture_of_prime._proof_8 p hp1 hq_ne2))⊢ q < p H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ hq_dvd))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * shs_odd:Odd s := (Nat.odd_mul.mp (hs ▸ hp_odd)).righth3q:3 ∣ 2 ^ q + 1 := new_mersenne_conjecture_of_prime._proof_6 p hq_oddh3p:3 ∣ 2 ^ p + 1 := Dvd.dvd.trans h3q hpow_dvdk:ℕhk:2 ^ p + 1 = (2 ^ q + 1) * kd:ℕ := (2 ^ q + 1) / 3hd:d = (2 ^ q + 1) / 3 := rflhd_dvd:d ∣ (2 ^ p + 1) / 3 := Exists.intro k (new_mersenne_conjecture_of_prime._proof_7 p h3q k hk)h8:8 ≤ 2 ^ q := Trans.trans (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8)) (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)) (Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit1))) (Nat.pow_le_pow_right (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)) (new_mersenne_conjecture_of_prime._proof_8 p hp1 hq_ne2))⊢ 1 < 2H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ hq_dvd))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * shs_odd:Odd s := (Nat.odd_mul.mp (hs ▸ hp_odd)).righth3q:3 ∣ 2 ^ q + 1 := new_mersenne_conjecture_of_prime._proof_6 p hq_oddh3p:3 ∣ 2 ^ p + 1 := Dvd.dvd.trans h3q hpow_dvdk:ℕhk:2 ^ p + 1 = (2 ^ q + 1) * kd:ℕ := (2 ^ q + 1) / 3hd:d = (2 ^ q + 1) / 3 := rflhd_dvd:d ∣ (2 ^ p + 1) / 3 := Exists.intro k (new_mersenne_conjecture_of_prime._proof_7 p h3q k hk)h8:8 ≤ 2 ^ q := Trans.trans (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8)) (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)) (Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit1))) (Nat.pow_le_pow_right (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)) (new_mersenne_conjecture_of_prime._proof_8 p hp1 hq_ne2))⊢ q < p All goals completed! 🐙 All goals completed! 🐙 H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ hq_dvd))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * shs_odd:Odd s := (Nat.odd_mul.mp (hs ▸ hp_odd)).righth3q:3 ∣ 2 ^ q + 1 := new_mersenne_conjecture_of_prime._proof_6 p hq_oddh3p:3 ∣ 2 ^ p + 1 := Dvd.dvd.trans h3q hpow_dvdk:ℕhk:2 ^ p + 1 = (2 ^ q + 1) * kd:ℕ := (2 ^ q + 1) / 3hd:d = (2 ^ q + 1) / 3 := rflhd_dvd:d ∣ (2 ^ p + 1) / 3 := Exists.intro k (new_mersenne_conjecture_of_prime._proof_7 p h3q k hk)h8:8 ≤ 2 ^ q := Trans.trans (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8)) (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)) (Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit1))) (Nat.pow_le_pow_right (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)) (new_mersenne_conjecture_of_prime._proof_8 p hp1 hq_ne2))hd_lt:d < (2 ^ p + 1) / 3 := have hpow := Nat.pow_lt_pow_right new_mersenne_conjecture_of_prime._proof_9 (new_mersenne_conjecture_of_prime._proof_10 p hp_odd hp_prime hp1); new_mersenne_conjecture_of_prime._proof_11 p h3p hpowh:d = 1⊢ FalseH:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ hq_dvd))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * shs_odd:Odd s := (Nat.odd_mul.mp (hs ▸ hp_odd)).righth3q:3 ∣ 2 ^ q + 1 := new_mersenne_conjecture_of_prime._proof_6 p hq_oddh3p:3 ∣ 2 ^ p + 1 := Dvd.dvd.trans h3q hpow_dvdk:ℕhk:2 ^ p + 1 = (2 ^ q + 1) * kd:ℕ := (2 ^ q + 1) / 3hd:d = (2 ^ q + 1) / 3 := rflhd_dvd:d ∣ (2 ^ p + 1) / 3 := Exists.intro k (new_mersenne_conjecture_of_prime._proof_7 p h3q k hk)h8:8 ≤ 2 ^ q := Trans.trans (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8)) (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)) (Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit1))) (Nat.pow_le_pow_right (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)) (new_mersenne_conjecture_of_prime._proof_8 p hp1 hq_ne2))hd_lt:d < (2 ^ p + 1) / 3 := have hpow := Nat.pow_lt_pow_right new_mersenne_conjecture_of_prime._proof_9 (new_mersenne_conjecture_of_prime._proof_10 p hp_odd hp_prime hp1); new_mersenne_conjecture_of_prime._proof_11 p h3p hpowh:d = (2 ^ p + 1) / 3⊢ False H:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ hq_dvd))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * shs_odd:Odd s := (Nat.odd_mul.mp (hs ▸ hp_odd)).righth3q:3 ∣ 2 ^ q + 1 := new_mersenne_conjecture_of_prime._proof_6 p hq_oddh3p:3 ∣ 2 ^ p + 1 := Dvd.dvd.trans h3q hpow_dvdk:ℕhk:2 ^ p + 1 = (2 ^ q + 1) * kd:ℕ := (2 ^ q + 1) / 3hd:d = (2 ^ q + 1) / 3 := rflhd_dvd:d ∣ (2 ^ p + 1) / 3 := Exists.intro k (new_mersenne_conjecture_of_prime._proof_7 p h3q k hk)h8:8 ≤ 2 ^ q := Trans.trans (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8)) (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)) (Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit1))) (Nat.pow_le_pow_right (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)) (new_mersenne_conjecture_of_prime._proof_8 p hp1 hq_ne2))hd_lt:d < (2 ^ p + 1) / 3 := have hpow := Nat.pow_lt_pow_right new_mersenne_conjecture_of_prime._proof_9 (new_mersenne_conjecture_of_prime._proof_10 p hp_odd hp_prime hp1); new_mersenne_conjecture_of_prime._proof_11 p h3p hpowh:d = 1⊢ FalseH:∀ (p : ℕ), Nat.Prime p → NewMersenneConjectureStatement pp:ℕhp_odd:Odd php_prime:¬Nat.Prime pleft✝:Odd phP:Nat.Prime ((2 ^ p + 1) / 3)hp1:¬p = 1q:ℕ := p.minFachq_ne2:q ≠ 2 := fun h => Nat.not_even_iff_odd.mpr hp_odd (even_iff_two_dvd.mpr (h ▸ hq_dvd))hq_odd:Odd q := Nat.Prime.odd_of_ne_two (Nat.minFac_prime hp1) hq_ne2s:ℕhs:p = q * shs_odd:Odd s := (Nat.odd_mul.mp (hs ▸ hp_odd)).righth3q:3 ∣ 2 ^ q + 1 := new_mersenne_conjecture_of_prime._proof_6 p hq_oddh3p:3 ∣ 2 ^ p + 1 := Dvd.dvd.trans h3q hpow_dvdk:ℕhk:2 ^ p + 1 = (2 ^ q + 1) * kd:ℕ := (2 ^ q + 1) / 3hd:d = (2 ^ q + 1) / 3 := rflhd_dvd:d ∣ (2 ^ p + 1) / 3 := Exists.intro k (new_mersenne_conjecture_of_prime._proof_7 p h3q k hk)h8:8 ≤ 2 ^ q := Trans.trans (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8)) (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)) (Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit1))) (Nat.pow_le_pow_right (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)) (new_mersenne_conjecture_of_prime._proof_8 p hp1 hq_ne2))hd_lt:d < (2 ^ p + 1) / 3 := have hpow := Nat.pow_lt_pow_right new_mersenne_conjecture_of_prime._proof_9 (new_mersenne_conjecture_of_prime._proof_10 p hp_odd hp_prime hp1); new_mersenne_conjecture_of_prime._proof_11 p h3p hpowh:d = (2 ^ p + 1) / 3⊢ False All goals completed! 🐙

The New Mersenne Conjecture statement holds for odd primes.

@[category research open, AMS 11] theorem declaration uses 'sorry'new_mersenne_conjecture.variants.prime (p : ℕ) (hp : p.Prime) (h : Odd p) : NewMersenneConjectureStatement p := p:ℕhp:Nat.Prime ph:Odd p⊢ NewMersenneConjectureStatement p All goals completed! 🐙

Are there infinitely many Mersenne primes?

@[category research open, AMS 11] theorem declaration uses 'sorry'infinitely_many_mersenne_primes : answer(sorry) ↔ Set.Infinite { p : ℕ | (mersenne p).Prime } := ⊢ True ↔ {p | Nat.Prime (mersenne p)}.Infinite All goals completed! 🐙

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?

@[category research open, AMS 11] theorem declaration uses 'sorry'catalans_mersenne_conjecture : answer(sorry) ↔ ∀ n ≥ 5, Nat.Prime (catalanMersenne n) := ⊢ True ↔ ∀ n ≥ 5, Nat.Prime (catalanMersenne n) All goals completed! 🐙 end Mersenne