fermat_four
plain-language theorem explainer
65537 is asserted to be prime as the fourth Fermat number F_4. Number theorists checking small cases in Fermat prime lists or arithmetic progressions would cite the fact for verification. The proof proceeds by a single native_decide tactic that evaluates the expression and confirms primality directly.
Claim. $2^{2^4} + 1 = 65537$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and keeping statements minimal to support later Dirichlet inversion layers. The local setting is basic interface stabilization rather than full algebraic development. Prime is the transparent alias for the standard Nat.Prime predicate on natural numbers.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to compute the value of 2^(2^4)+1 and verify its primality at the meta level.
why it matters
The declaration supplies a concrete verified instance of F_4 within the primes arithmetic functions section. No downstream uses appear in the used_by edges. It fills a specific computational case in the number-theoretic scaffolding but does not connect to the Möbius or inversion machinery developed in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.