theorem
proved
weak_prime_sixtyone
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 2771.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2768theorem weak_prime_fortyseven : Prime 47 ∧ Prime 43 ∧ Prime 53 ∧ 47 < (43 + 53) / 2 := by native_decide
2769
2770/-- 61 is a weak prime: 61 < (59 + 67)/2 = 63. -/
2771theorem weak_prime_sixtyone : Prime 61 ∧ Prime 59 ∧ Prime 67 ∧ 61 < (59 + 67) / 2 := by native_decide
2772
2773/-- 73 is a weak prime: 73 < (71 + 79)/2 = 75. -/
2774theorem weak_prime_seventythree : Prime 73 ∧ Prime 71 ∧ Prime 79 ∧ 73 < (71 + 79) / 2 := by native_decide
2775
2776/-- 83 is a weak prime: 83 < (79 + 89)/2 = 84. -/
2777theorem weak_prime_eightythree : Prime 83 ∧ Prime 79 ∧ Prime 89 ∧ 83 < (79 + 89) / 2 := by native_decide
2778
2779/-- 89 is a weak prime: 89 < (83 + 97)/2 = 90. -/
2780theorem weak_prime_eightynine : Prime 89 ∧ Prime 83 ∧ Prime 97 ∧ 89 < (83 + 97) / 2 := by native_decide
2781
2782/-- 103 is a weak prime: 103 < (101 + 107)/2 = 104 (RS-relevant). -/
2783theorem weak_prime_onehundredthree : Prime 103 ∧ Prime 101 ∧ Prime 107 ∧ 103 < (101 + 107) / 2 := by native_decide
2784
2785/-! ### Superprimes (prime-indexed primes: p_n where n is also prime) -/
2786
2787/-- p_2 = 3 is a superprime. -/
2788theorem superprime_three : Prime 3 ∧ Prime 2 := by native_decide
2789
2790/-- p_3 = 5 is a superprime. -/
2791theorem superprime_five : Prime 5 ∧ Prime 3 := by native_decide
2792
2793/-- p_5 = 11 is a superprime (RS-relevant). -/
2794theorem superprime_eleven : Prime 11 ∧ Prime 5 := by native_decide
2795
2796/-- p_7 = 17 is a superprime (RS-relevant). -/
2797theorem superprime_seventeen : Prime 17 ∧ Prime 7 := by native_decide
2798
2799/-- p_11 = 31 is a superprime. -/
2800theorem superprime_thirtyone : Prime 31 ∧ Prime 11 := by native_decide
2801