theorem
proved
four_almost_prime_onehundred
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 2255.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2252theorem four_almost_prime_ninety : isFourAlmostPrime 90 = true := by native_decide
2253
2254/-- 100 = 2² × 5² is 4-almost prime. -/
2255theorem four_almost_prime_onehundred : isFourAlmostPrime 100 = true := by native_decide
2256
2257/-- 104 = 2³ × 13 is 4-almost prime. -/
2258theorem four_almost_prime_onehundredfour : isFourAlmostPrime 104 = true := by native_decide
2259
2260-- Note: 120 = 2³ × 3 × 5, Ω = 3 + 1 + 1 = 5, so 120 is 5-almost prime, not 4-almost prime
2261
2262/-- 126 = 2 × 3² × 7 is 4-almost prime. -/
2263theorem four_almost_prime_onehundredtwentysix : isFourAlmostPrime 126 = true := by native_decide
2264
2265/-- 132 = 2² × 3 × 11 is 4-almost prime (RS-relevant: 11). -/
2266theorem four_almost_prime_onehundredthirtytwo : isFourAlmostPrime 132 = true := by native_decide
2267
2268/-- 136 = 2³ × 17 is 4-almost prime (RS-relevant: 17). -/
2269theorem four_almost_prime_onehundredthirtysix : isFourAlmostPrime 136 = true := by native_decide
2270
2271/-- 140 = 2² × 5 × 7 is 4-almost prime. -/
2272theorem four_almost_prime_onehundredforty : isFourAlmostPrime 140 = true := by native_decide
2273
2274/-! ### Chen primes (p is prime and p+2 is prime or semiprime) -/
2275
2276/-- 2 is a Chen prime: 2+2 = 4 = 2² is semiprime. -/
2277theorem chen_prime_two : Prime 2 ∧ isSemiprime 4 = true := by native_decide
2278
2279/-- 3 is a Chen prime: 3+2 = 5 is prime. -/
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. -/