prime_fivehundredeightyseven
plain-language theorem explainer
587 is asserted to be a prime number inside the arithmetic functions module. Number theorists checking Möbius sums or squarefree properties in the Recognition Science setup would reference this fact for exact integer inputs. The proof is a one-line native_decide call that delegates the primality test to the computational engine.
Claim. $587$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for Nat.Prime. The local setting keeps statements minimal so that Dirichlet inversion and related algebra can be added once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to confirm 587 satisfies the Nat.Prime predicate.
why it matters
This supplies a verified prime fact inside the NumberTheory.Primes submodule. No downstream theorems currently cite it, so it functions as a checked constant for potential arithmetic-function calculations. It touches the framework's requirement for exact number-theoretic building blocks but does not engage the forcing chain or J-cost directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.