strong_prime_fiftynine
plain-language theorem explainer
The statement verifies that 59 is a strong prime by confirming primality of 59, 53, and 61 together with the inequality placing 59 strictly above their average. Number theorists referencing concrete prime-gap examples or strong-prime instances in arithmetic contexts would cite this numerical anchor. The proof reduces to a single native decision procedure that evaluates the finite arithmetic claim directly.
Claim. $59$ is prime, $53$ is prime, $61$ is prime, and $59 > (53 + 61)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the repo-local alias for the standard Nat.Prime predicate. The local setting keeps statements minimal, deferring deeper Dirichlet algebra until basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to discharge the arithmetic statement.
why it matters
This supplies a verified concrete instance of a strong prime inside the NumberTheory.Primes hierarchy. It anchors numerical facts that may feed later arithmetic-function calculations, though no downstream usage is recorded. It aligns with the framework's pattern of explicit numerical checks supporting prime-related constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.