chen_prime_fortyone
plain-language theorem explainer
The declaration establishes that both 41 and 43 are prime numbers, confirming 41 as a Chen prime. Number theorists examining small prime pairs or explicit instances in Chen's theorem would reference this fact. The proof is a direct computational check via native_decide on the primality predicates.
Claim. $41$ and $43$ are both prime numbers.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. The local setting keeps statements minimal to allow layering of Dirichlet algebra later. The Prime predicate is the repo-local alias for the standard Nat.Prime predicate on natural numbers.
proof idea
The proof is a one-line term that invokes native_decide to evaluate the conjunction of the primality checks for 41 and 43.
why it matters
This supplies a concrete Chen prime instance inside the arithmetic functions module. It populates basic facts in the NumberTheory.Primes section of the Recognition framework, supporting any later constructions that rely on explicit small primes. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.