safe_prime_twentythree
plain-language theorem explainer
The declaration verifies that 23 and 11 are both prime, confirming 23 as a safe prime. Number theorists checking small cases of safe primes or Sophie Germain primes would cite this computational fact. The proof reduces the conjunction to a single native decision procedure on natural-number predicates.
Claim. $23$ is prime and $11$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard predicate that a natural number has no divisors other than 1 and itself. The local setting is basic number-theoretic scaffolding before deeper Dirichlet inversion is added.
proof idea
The proof is a one-line wrapper that applies native_decide to discharge the primality statements by direct computation.
why it matters
The result supplies a verified small safe-prime instance inside the NumberTheory.Primes section. It feeds no downstream theorems in the current graph and touches no Recognition Science landmarks such as the forcing chain or RCL. It functions as an empirical foothold for later arithmetic-function work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.