Wikipedia · textbook · AMS 11
mediumknown result, no worker yet
Conjectures about Mersenne primes
Theorem · new_mersenne_conjecture_of_prime
It suffices to check this conjecture for odd primes. The statement fails at p = 2:
mersenne 2 = 3 is prime and 2 = 2 ^ 0 + 1, but 2 gives no Wagstaff prime.
Formal statement · Lean 4.lean
theorem new_mersenne_conjecture_of_prime :
(∀ p, p.Prime → Odd p → NewMersenneConjectureStatement p) →
∀ p, Odd p → NewMersenneConjectureStatement p := by
sorryProof. sorry
Nobody has tried yet.