sophie_germain_twentythree
plain-language theorem explainer
23 is a Sophie Germain prime, so both 23 and 47 are prime. Number theorists verifying small prime pairs for arithmetic-function calculations would cite the fact. The proof is a one-line native decision that directly evaluates the two primality predicates.
Claim. $23$ is prime and $2·23+1=47$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the repository-local transparent alias for the standard Nat.Prime predicate. This explicit check sits among the prime facts that support those arithmetic-function interfaces.
proof idea
The proof is a one-line wrapper that invokes native_decide on the conjunction of the two primality statements.
why it matters
The declaration supplies a concrete verified instance inside the primes module that can feed arithmetic-function lemmas. It has no listed dependents, so its role is limited to scaffolding small-case checks rather than advancing the Recognition Science forcing chain or J-cost relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.