theorem
proved
weak_prime_eightythree
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 2777.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
2802/-- p_13 = 41 is a superprime. -/
2803theorem superprime_fortyone : Prime 41 ∧ Prime 13 := by native_decide
2804
2805/-- p_17 = 59 is a superprime. -/
2806theorem superprime_fiftynine : Prime 59 ∧ Prime 17 := by native_decide
2807