prime_sixhundredeightythree
plain-language theorem explainer
The declaration establishes that 683 is a prime number. Number theorists using arithmetic functions such as the Möbius function in sums over primes would cite this fact for concrete verification in calculations. The proof is a direct computational check via native decision procedures.
Claim. $683$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. Prime is the standard predicate for natural-number primality. Upstream results supply basic structures ensuring collision-free properties and algebraic tautologies in the broader framework, along with the transparent alias for the primality predicate.
proof idea
The proof is a one-line wrapper that applies native_decide to verify the primality of 683 directly.
why it matters
This theorem supplies a concrete prime fact inside the arithmetic functions module to support Möbius-function computations on primes. It sits within the Recognition Science number-theory layer that feeds prime distributions and related constants, though it records no downstream uses and functions as a verified basic fact rather than a core lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.