chen_prime_twentynine
plain-language theorem explainer
The declaration asserts that both 29 and 31 are prime numbers, supplying an explicit base case for Chen prime verification in the arithmetic functions module. Number theorists checking small twin-prime pairs or semiprime gaps would cite it for direct confirmation. The proof applies a native decision procedure that evaluates the primality predicates by computation.
Claim. The integers 29 and 31 are both prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard Nat.Prime predicate. Upstream results include the basic Prime abbrev together with structural is theorems from foundation modules that record collision-free or tautological properties.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the conjunction of the two primality checks directly.
why it matters
The result supplies the explicit small-case verification that 29 is a Chen prime because 31 is prime, as stated in the declaration comment. It sits inside the arithmetic-functions scaffolding of the NumberTheory section, though no downstream uses are recorded yet. It aligns with the framework's pattern of concrete checks before layering Dirichlet inversion or larger prime-gap arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.