theorem
proved
four_almost_prime_eightyfour
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 2246.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2243theorem four_almost_prime_eightyone : isFourAlmostPrime 81 = true := by native_decide
2244
2245/-- 84 = 2² × 3 × 7 is 4-almost prime. -/
2246theorem four_almost_prime_eightyfour : isFourAlmostPrime 84 = true := by native_decide
2247
2248/-- 88 = 2³ × 11 is 4-almost prime (RS-relevant: 11). -/
2249theorem four_almost_prime_eightyeight : isFourAlmostPrime 88 = true := by native_decide
2250
2251/-- 90 = 2 × 3² × 5 is 4-almost prime. -/
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. -/