cousin_prime_thirtyseven_fortyone
plain-language theorem explainer
37 and 41 form a cousin prime pair differing by 4. Researchers checking small prime constellations or supplying concrete inputs to arithmetic-function lemmas would cite this instance. The proof executes as a direct native_decide term that evaluates the primality predicates and the offset equality for these fixed integers.
Claim. The integers $37$ and $41$ are both prime and satisfy $41 = 37 + 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the module-local alias for the standard primality predicate on natural numbers. The upstream CirclePhaseLift.and supplies the conjunction connective used in the statement, while the Basic.Prime alias provides the predicate itself.
proof idea
The proof is a one-line term that applies native_decide to evaluate the conjunction of the two primality checks and the arithmetic equality on the concrete constants 37 and 41.
why it matters
The declaration supplies a verified small-case fact about cousin primes inside the arithmetic-functions module. It serves as a basic number-theoretic foothold before deeper Dirichlet algebra or Möbius inversion is layered on, consistent with the module's stated lightweight-interface goal. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.