theorem
proved
chen_prime_five
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 2283.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2280theorem chen_prime_three : Prime 3 ∧ Prime 5 := by native_decide
2281
2282/-- 5 is a Chen prime: 5+2 = 7 is prime. -/
2283theorem chen_prime_five : Prime 5 ∧ Prime 7 := by native_decide
2284
2285/-- 7 is a Chen prime: 7+2 = 9 = 3² is semiprime. -/
2286theorem chen_prime_seven : Prime 7 ∧ isSemiprime 9 = true := by native_decide
2287
2288/-- 11 is a Chen prime: 11+2 = 13 is prime (RS-relevant). -/
2289theorem chen_prime_eleven : Prime 11 ∧ Prime 13 := by native_decide
2290
2291/-- 13 is a Chen prime: 13+2 = 15 = 3×5 is semiprime. -/
2292theorem chen_prime_thirteen : Prime 13 ∧ isSemiprime 15 = true := by native_decide
2293
2294/-- 17 is a Chen prime: 17+2 = 19 is prime (RS-relevant). -/
2295theorem chen_prime_seventeen : Prime 17 ∧ Prime 19 := by native_decide
2296
2297/-- 19 is a Chen prime: 19+2 = 21 = 3×7 is semiprime. -/
2298theorem chen_prime_nineteen : Prime 19 ∧ isSemiprime 21 = true := by native_decide
2299
2300/-- 23 is a Chen prime: 23+2 = 25 = 5² is semiprime. -/
2301theorem chen_prime_twentythree : Prime 23 ∧ isSemiprime 25 = true := by native_decide
2302
2303/-- 29 is a Chen prime: 29+2 = 31 is prime. -/
2304theorem chen_prime_twentynine : Prime 29 ∧ Prime 31 := by native_decide
2305
2306/-- 31 is a Chen prime: 31+2 = 33 = 3×11 is semiprime. -/
2307theorem chen_prime_thirtyone : Prime 31 ∧ isSemiprime 33 = true := by native_decide
2308
2309/-- 37 is a Chen prime: 37+2 = 39 = 3×13 is semiprime (RS-relevant). -/
2310theorem chen_prime_thirtyseven : Prime 37 ∧ isSemiprime 39 = true := by native_decide
2311
2312/-- 41 is a Chen prime: 41+2 = 43 is prime. -/
2313theorem chen_prime_fortyone : Prime 41 ∧ Prime 43 := by native_decide