chen_prime_twentythree
plain-language theorem explainer
23 is prime and 25 has exactly two prime factors counted with multiplicity, confirming the Chen prime property for 23. Number theorists examining explicit cases in bounded prime gaps or Chen's theorem would cite this instance. The proof is a one-line wrapper that applies native_decide for direct computational verification.
Claim. 23 is prime and $25$ is semiprime, i.e., $23$ satisfies the standard primality predicate while $25$ satisfies $Omega(25)=2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard primality predicate on natural numbers. isSemiprime is the Boolean check that bigOmega n equals 2, where bigOmega counts prime factors with multiplicity; the supplied snippet states a number is semiprime precisely when this count is two.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the conjunction of primality for 23 and the semiprime predicate for 25 by direct computation.
why it matters
This supplies a concrete verified example inside the arithmetic functions layer that supports Möbius footholds and related number-theoretic tools. No downstream theorems appear in the used_by edges, so it currently functions as an isolated instance rather than feeding a parent result. It illustrates the semiprime definition in a Chen-prime context without yet touching Recognition Science landmarks such as the J-uniqueness step or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.