twin_prime_seventyone_seventythree
plain-language theorem explainer
71 and 73 form a twin prime pair. Number theorists checking small prime values inside the arithmetic functions module would cite this fact. The proof reduces to a single native_decide invocation that verifies both primality statements and the exact difference of 2.
Claim. $71$ is prime, $73$ is prime, and $73 = 71 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. This theorem supplies a concrete twin prime pair for use when evaluating functions at small integers. It rests on the upstream alias Prime, defined as the standard predicate Nat.Prime n.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to decide the conjunction of primality and equality statements computationally.
why it matters
This theorem supplies a verified twin prime pair inside the arithmetic functions module. It populates a concrete data point for later prime-factor or Möbius computations at RS-related numbers, though the used_by graph records no downstream applications yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.