chen_prime_thirtyone
plain-language theorem explainer
31 is prime and 33 is semiprime, confirming 31 as a Chen prime via the difference of 2. Number theorists studying bounded prime gaps or Chen's theorem would cite this concrete case. The proof applies a native decision procedure that evaluates the conjunction directly.
Claim. 31 is prime and the total number of prime factors of 33 counted with multiplicity equals 2.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the standard primality predicate on natural numbers. isSemiprime holds exactly when bigOmega n equals 2, i.e., the number has precisely two prime factors counting multiplicity.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the primality of 31 and the semiprimality of 33 by direct computation.
why it matters
This supplies a verified Chen-prime instance inside the arithmetic-functions development. The module keeps statements lightweight pending deeper Dirichlet algebra. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.