twin_prime_threehundredfortyseven_threehundredfortynine
plain-language theorem explainer
The declaration asserts that 347 and 349 are both prime and differ by exactly 2. Number theorists or framework developers needing verified small twin-prime instances for arithmetic checks would reference it. The proof is a one-line native_decide that evaluates the primality predicates and the difference equation directly.
Claim. $347$ and $349$ are both prime numbers with $349 = 347 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is defined as the transparent alias abbrev Prime (n : ℕ) : Prop := Nat.Prime n. The local setting is a collection of small statements on primes and squarefree numbers that can later support Dirichlet inversion or related algebra.
proof idea
One-line wrapper that applies native_decide to the conjunction of the two primality statements and the arithmetic equality.
why it matters
Supplies a concrete verified twin-prime pair inside the NumberTheory.Primes section. No downstream uses are recorded, so it functions as a basic numerical fact available for later arithmetic-function arguments or phi-ladder checks. It sits alongside the Möbius wrappers but does not invoke them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.