fermat_two
plain-language theorem explainer
Verification that 17 is prime as the Fermat number 2^(2^2) + 1 appears in the arithmetic functions library. Number theorists studying explicit primes or Fermat sequences would reference the result. Native decision computes the primality check without manual proof steps.
Claim. $2^{2^{2}} + 1$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The Prime predicate is the repo-local alias for Nat.Prime. Upstream results supply the transparent abbrev Prime (n : ℕ) : Prop := Nat.Prime n together with structural is theorems from foundation modules that enforce collision-free or tautological properties.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the primality predicate directly on the concrete numeral.
why it matters
The declaration supplies an explicit verified Fermat prime inside the arithmetic-functions module. No downstream uses are recorded. It contributes a concrete instance to the number-theory layer that supports later prime constructions without touching the forcing chain or RS constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.