theorem
proved
superprime_onehundredninetyone
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 2827.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2824theorem superprime_onehundredseventynine : Prime 179 ∧ Prime 41 := by native_decide
2825
2826/-- p_43 = 191 is a superprime. -/
2827theorem superprime_onehundredninetyone : Prime 191 ∧ Prime 43 := by native_decide
2828
2829/-- p_47 = 211 is a superprime. -/
2830theorem superprime_twohundredeleven : Prime 211 ∧ Prime 47 := by native_decide
2831
2832/-! ### Isolated primes (no twin: p-2 and p+2 both composite) -/
2833
2834/-- 23 is an isolated prime: 21 = 3 × 7, 25 = 5². -/
2835theorem isolated_prime_twentythree : Prime 23 ∧ ¬Prime 21 ∧ ¬Prime 25 := by native_decide
2836
2837/-- 37 is an isolated prime: 35 = 5 × 7, 39 = 3 × 13 (RS-relevant). -/
2838theorem isolated_prime_thirtyseven : Prime 37 ∧ ¬Prime 35 ∧ ¬Prime 39 := by native_decide
2839
2840/-- 47 is an isolated prime: 45 = 3² × 5, 49 = 7². -/
2841theorem isolated_prime_fortyseven : Prime 47 ∧ ¬Prime 45 ∧ ¬Prime 49 := by native_decide
2842
2843/-- 53 is an isolated prime: 51 = 3 × 17, 55 = 5 × 11. -/
2844theorem isolated_prime_fiftythree : Prime 53 ∧ ¬Prime 51 ∧ ¬Prime 55 := by native_decide
2845
2846/-- 67 is an isolated prime: 65 = 5 × 13, 69 = 3 × 23. -/
2847theorem isolated_prime_sixtyseven : Prime 67 ∧ ¬Prime 65 ∧ ¬Prime 69 := by native_decide
2848
2849/-- 79 is an isolated prime: 77 = 7 × 11, 81 = 3⁴. -/
2850theorem isolated_prime_seventynine : Prime 79 ∧ ¬Prime 77 ∧ ¬Prime 81 := by native_decide
2851
2852/-- 83 is an isolated prime: 81 = 3⁴, 85 = 5 × 17. -/
2853theorem isolated_prime_eightythree : Prime 83 ∧ ¬Prime 81 ∧ ¬Prime 85 := by native_decide
2854
2855/-- 89 is an isolated prime: 87 = 3 × 29, 91 = 7 × 13. -/
2856theorem isolated_prime_eightynine : Prime 89 ∧ ¬Prime 87 ∧ ¬Prime 91 := by native_decide
2857