theorem
proved
superprime_three
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 2788.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
2808/-- p_19 = 67 is a superprime. -/
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