theorem
proved
safe_prime_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 1426.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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. -/
1448theorem abundant_thirty : sigma 1 30 > 2 * 30 := by native_decide
1449
1450/-- 36 is abundant: σ_1(36) = 91 > 72. -/
1451theorem abundant_thirtysix : sigma 1 36 > 2 * 36 := by native_decide
1452
1453/-! ### Deficient numbers (σ_1(n) < 2n) -/
1454
1455/-- 1 is deficient: σ_1(1) = 1 < 2. -/
1456theorem deficient_one : sigma 1 1 < 2 * 1 := by native_decide