emirp_seventyone
plain-language theorem explainer
71 reversed is the distinct prime 17. Researchers cataloging small emirps or verifying explicit prime pairs cite this instance. The proof executes as a single native_decide call that computes the primality predicates and inequality directly.
Claim. $71$ is prime, $17$ is prime, and $71 ≠ 17$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and basic squarefree checks. The local setting keeps statements minimal until Dirichlet inversion layers stabilize. Prime is the transparent alias for Nat.Prime, permitting direct use of standard primality without additional hypotheses.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the conjunction of the two primality statements and the inequality.
why it matters
This supplies a concrete verified emirp instance inside the arithmetic functions module. It supports the number theory scaffolding that may feed later prime constructions, though the dependency graph records no downstream uses. The placement aligns with the emphasis on explicit small-case checks before deeper algebraic development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.