theorem
proved
safe_prime_twentythree
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 1417.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1414theorem safe_prime_eleven : Prime 11 ∧ Prime ((11 - 1) / 2) := by native_decide
1415
1416/-- 23 is a safe prime: (23-1)/2 = 11 is prime. -/
1417theorem safe_prime_twentythree : Prime 23 ∧ Prime ((23 - 1) / 2) := by native_decide
1418
1419/-- 47 is a safe prime: (47-1)/2 = 23 is prime. -/
1420theorem safe_prime_fortyseven : Prime 47 ∧ Prime ((47 - 1) / 2) := by native_decide
1421
1422/-- 59 is a safe prime: (59-1)/2 = 29 is prime. -/
1423theorem safe_prime_fiftynine : Prime 59 ∧ Prime ((59 - 1) / 2) := by native_decide
1424
1425/-- 83 is a safe prime: (83-1)/2 = 41 is prime. -/
1426theorem safe_prime_eightythree : Prime 83 ∧ Prime ((83 - 1) / 2) := by native_decide
1427
1428-- Note: 89 is NOT a safe prime since (89-1)/2 = 44 = 4×11 is composite
1429
1430/-- 107 is a safe prime: (107-1)/2 = 53 is prime. -/
1431theorem safe_prime_onehundredseven : Prime 107 ∧ Prime ((107 - 1) / 2) := by native_decide
1432
1433/-! ### Abundant numbers (σ_1(n) > 2n) -/
1434
1435/-- 12 is abundant: σ_1(12) = 28 > 24. -/
1436theorem abundant_twelve : sigma 1 12 > 2 * 12 := by native_decide
1437
1438/-- 18 is abundant: σ_1(18) = 39 > 36. -/
1439theorem abundant_eighteen : sigma 1 18 > 2 * 18 := by native_decide
1440
1441/-- 20 is abundant: σ_1(20) = 42 > 40. -/
1442theorem abundant_twenty : sigma 1 20 > 2 * 20 := by native_decide
1443
1444/-- 24 is abundant: σ_1(24) = 60 > 48. -/
1445theorem abundant_twentyfour : sigma 1 24 > 2 * 24 := by native_decide
1446
1447/-- 30 is abundant: σ_1(30) = 72 > 60. -/