Primes_of_form_Power_of_Two_plus_One
Provedfermat-numbersprime-numbersproofwiki
Let n be a natural number. If 2^n + 1 is prime, then n is a power of 2.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Data.Nat.Prime.Basic
Formal statement
theorem Primes_of_form_Power_of_Two_plus_One (n : ℕ) (hn : 0 < n) (hp : Nat.Prime (2 ^ n + 1)) : ∃ k : ℕ, n = 2 ^ k := by sorry
Source