Prove that there are infinitely many Mersenne primes

Prove that there are arbitrarily large exponents p for which 2^p − 1 is prime. The statement also requires p itself to be prime, which is necessary for a Mersenne number to be prime. Natural subtraction is used, but primality and p ≥ 2 exclude the truncation edge cases. A prime-search record or probabilistic heuristic is not a proof of infinitude. Research status checked 8 October 2026: no accepted general proof identified in the cited literature. This is a proposed formal statement; independent correspondence review is requested. A successful statement check establishes well-formedness, not the conjecture.

(fun prime : Nat → Prop =>
  ∀ N : Nat, ∃ p : Nat, N < p ∧ prime p ∧ prime (2 ^ p - 1))
(fun p => 2 ≤ p ∧ ∀ d : Nat, d ∣ p → d = 1 ∨ d = p)

OA_statement : Prop