theorem
proved
superprime_eightythree
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 2812.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2809theorem superprime_sixtyseven : Prime 67 ∧ Prime 19 := by native_decide
2810
2811/-- p_23 = 83 is a superprime. -/
2812theorem superprime_eightythree : Prime 83 ∧ Prime 23 := by native_decide
2813
2814/-- p_29 = 109 is a superprime. -/
2815theorem superprime_onehundrednine : Prime 109 ∧ Prime 29 := by native_decide
2816
2817/-- p_31 = 127 is a superprime (also Mersenne prime 2^7 - 1). -/
2818theorem superprime_onehundredtwentyseven : Prime 127 ∧ Prime 31 := by native_decide
2819
2820/-- p_37 = 157 is a superprime (RS-relevant: 37). -/
2821theorem superprime_onehundredfiftyseven : Prime 157 ∧ Prime 37 := by native_decide
2822
2823/-- p_41 = 179 is a superprime. -/
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