mersenne_five
plain-language theorem explainer
mersenne_five asserts that 31 is prime. Number theorists examining Mersenne primes cite this explicit case as a verified instance. The proof executes via a native decision procedure that computes primality of the concrete integer directly.
Claim. $2^5 - 1 = 31$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the repo-local alias for the standard Nat.Prime predicate on natural numbers. Upstream results supply the basic primality definition together with foundational structures whose is predicates encode collision-free or tautological properties used in broader ledger and mechanism constructions.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the primality predicate on the explicit value 31.
why it matters
This supplies a concrete Mersenne prime instance inside the arithmetic-functions module. It supports downstream work on Möbius and related functions over primes, though no immediate parent theorems are recorded. The result sits alongside the module's Möbius footholds without touching the Recognition forcing chain or constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.