palindromic_prime_onehundredninetyone
plain-language theorem explainer
191 is asserted to be a prime natural number. Researchers listing small palindromic primes for arithmetic function checks would cite the result. The proof is a one-line term that invokes native_decide to settle the claim by direct computation.
Claim. The natural number 191 is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the local transparent alias for the standard Nat.Prime predicate on natural numbers. Upstream results supply structural definitions from foundation and game-theory modules, but the present theorem rests only on the primality predicate itself.
proof idea
The proof is a one-line term that applies native_decide to decide primality of 191 by computation.
why it matters
The theorem supplies a verified instance of a palindromic prime inside the primes module. It fills a basic fact without feeding any downstream theorem and without touching the Recognition Science forcing chain, J-uniqueness, or the phi-ladder. No open question is addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.